Finite axiomatization of NBG (VGB)

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.