Vgb-membership is the following theory:
Extensionality
Exist a set V such that:
V={x| Exist y (x in y)}
V is closed under set union, Boolean union, pairing, subsets and power, and has an element that is infinite.
For every element x of V there is a complementary set of x relative to V.
For all X,Y C V there intersection of X and Y exists
For all X,Y C V the Cartesian product of X and y exists
For all Y CV Exist X C V for all m,n,u ((m,n,u) in Y <-> (u,m,n) in X)
For all Y C V Exist X C V for all m,n,u ((m,n,u) in Y <-> (m,u,n) in X)
where m,n,n are all in V.
Now those are the finite axioms of Vgb the only one left is axiom of membership, so
the above is Vgb-membership, now clearly all of the above are theorems of NF, so the above is a proper fragment of NF, it is extensional and it is consistent with choice.
Â