Since I was not satisfied with the answers and comments obtained sofar, I decided to think on this question myself.

Here is the list of class existence axioms of NBG (written in an informal form):

**Axiom of Extensionality:** Two classes $X,Y$ are equal if and only if $X\subseteq Y$ and $Y\subseteq X$;

**Axiom of Memberships:** The class $E=\{(x,y):x\in y\}$ exists;

**Axiom of Intersection:** For any classes $X,Y$ the class $X\cap Y$ exists;

**Axiom of Complement:** For any classes $X,Y$ the class $X\setminus Y$ exists;

**Axiom of Domain:** For any class $X$ the class $dom[X]=\{x:\exists y\;(x,y)\in X\}$ exists;

**Axiom of Product by $V$:** For any class $X$ the class $X\times V$ exists;

**Axiom of Circular Permutation:** For any class $X$ the class $\{((x,y),z):((y,z),x)\in X\}$ exists;

**Axiom of Transposition:** For any class $X$ the class $\{((x,y),z):((x,z),y)\in X\}$ exists.

I claim that the Axiom of Transposition can be simplified to the following more natural form:

**Axiom of Inversion:** For any class $X$ the class $X^{-1}=\{(x,y):(y,x)\in X\}$ exists.

More precisely, I am going to prove the following

**Fact.** The Gödel's Axiom of Transposition can be deduced from the Axioms of Extensionality, Membership, Complement, Domain, Product, Circlular Permutation and Inversion.

The idea is to prove that the function $f:((x,y),z))\mapsto ((x,z),y)$ exists (as a class) and then observe that for any class $X$, the class $\{((x,y),z):((x,z),y)\in X\}$ coincides with the image $f[X]$, which is equal to $dom((f\cap (X\times V))^{-1})$ so exists by application of Axioms of Product, Intersection, Inversion, and Domain. As was observed by Emil Jeřábek in his comment, the Axiom of Intersection follows from the Axiom of Complement because $X\cap Y=X\setminus(X\setminus Y)$ for any classes $X,Y$.

It remains to prove that the function $f=\{((x,y),z),((x,z),y)):x,y,z\in V\}$ exists.
This will be done in a series of 10 lemmas.

Consider the functions $\pi_2:(x,y)\to(y,x)$ and $\pi_3:((x,y),z)\mapsto ((z,x),y)$ of transposition and cyclic permutation.

The Axioms of Inversion and Circular Permutation say that for any class $X$ the classes $\pi_2[X]$, $\pi_3[X]$, and $\pi_3^2[X]=\pi_3[\pi_3[X]]$ exist. (At the moment we do not claim that the functions $\pi_2$ and $\pi_3$ exist as classes).

**Lemma 1.** The class $S=\{(x,y):x\subseteq y\}$ exists.

*Proof.* Observe that $V\setminus S=dom(A\cap B)$ where $A=\{((x,y),z):z\in x\}$ and $B=\{((x,y),z):z\notin y\}$.

Observe that $\pi_3[A]=\{((z,x),y):z\in x\}=E\times V$ and hence $\pi_3[A]$ exists by the Axioms of Memberships and Product by $V$. Then $A$ exists by the Axiom of Circular Permutation.

Next, the class $\pi^2_3[B]=\{((y,z),x):z\notin y\}=(\pi_2[V\setminus E])\times V$ exists by the Axioms of Memberships, Complement, Inversion and Product by $V$. Applying the Axiom of Circular Permutation, we obtain that the class $B$ exists. Then $A\cap B$ exists by Axiom of Intersection, $V\setminus S=dom(A\cap B)$ exists by Axiom of Domain and $S$ exists by Axiom of Complement. $\quad\square$

**Lemma 2.** The class $I=\{(x,y):x=y\}$ describing the identity function $I:x\mapsto x$, exists.

*Proof.* By Lemma 1, the class $S=\{(x,y):x\subseteq y\}$ exists. Since $I=S\cap\pi_2[S]$ (by the Axiom of Extensionality), the class $I$ exists by the Axioms of Inversion and Intersection. $\quad\square$

The short proofs of the following five lemmas were suggested by Pace Nielsen in his comments below.

**Lemma 3.** The class $p_1=\{((a,b),a):a,b\in V\}$ describing the function $p_1:(a,b)\mapsto a$ exists.

*Proof.* Observe that $\pi_3[p_1]=\{((a,a),b):a,b\in V\}=I\times V$, so the classes $\pi_3[p_1]$ and $p_1=\pi_3^2[\pi_3[p_1]]$ exist. $\quad\square$

**Lemma 4.** The class $p_2=\{((a,b),b):a,b\in V\}$ describing the function $p_2:(a,b)\mapsto b$ exists.

*Proof.* Observe that $\pi^2_3[p_2]=\{((b,b),a):a,b\in V\}=I\times V$, so the class $p_2$ exists. $\quad\square$

**Lemma 5.** The class $pr_1=\{(((a,b),c),a):a,b,c\in V\}$ describing the function $pr_1:((a,b),c)\mapsto a$ exists.

*Proof.* Observe that $\pi_3[pr_1]=\{((a,(a,b)),c):a,b,c\in V\}=\pi_2[p_1]\times V$ and hence the classes $\pi_3[pr_1]$ and $pr_1$ exist by Lemma 4 and Axioms of Inversion, Product, and Circular Permutation.
$\quad\square$

**Lemma 6.** The class $pr_2=\{(((a,b),c),b):a,b,c\in V\}$ describing the function $pr_2:((a,b),c)\mapsto b$ exists.

*Proof.* Observe that $\pi_3[pr_2]=\{((b,(a,b)),c):a,b,c\in V\}=\pi_2[p_2]\times V$ and hence the classes $\pi_3[pr_2]$ exist by Lemma 4 and Axioms of Inversion, Product, and Circular Permutation. $\quad\square$

**Lemma 7.** The class $pr_3=\{(((a,b),c),c):a,b,c\in V\}$ describing the function $pr_1:((a,b),c)\mapsto c$ exists.

*Proof.* Observe that $\pi^{-1}_3[pr_3]=\{((c,c),(a,b)):a,b,c\in V\}=I\times(V\times V)$ and hence the class $pr_3$ exists by Lemma 2 and the Axiom of Product by $V$. $\quad\square$

**Lemma 8.** For any functions $F,G$ the class $\{x\in dom[F]\cap dom[G]:F(x)=G(x)\}$ exists.

*Proof.* Observe that $\{x\in dom[F]\cap dom[G]:F(x)=G(x)\}=dom[F\cap G]$ and apply the Axioms of Intersection and Domain. $\quad\square$

**Lemma 9.** For any functions $F,G$ the function
$F\circ G=\{(x,z):\exists y\;((x,y)\in G\;\wedge\;(y,z)\in F)\}$ exists.

*Proof.* Observe that $F\circ G=dom[A_1\cap A_2]$ where $A_1=\{((x,z),y):(x,y)\in G\}$ and $A_2=\{(x,z,y):(y,z)\in F\}$.

The class $\pi_3[A_1]=\{((y,x),z):(x,y)\in G\}=G^{-1}\times V$ exists by the Axioms of Inversion and Product.

The class $\pi^2_3[A_2]=\{((z,y),x):(y,z)\in F\}=F^{-1}\times V$ exists by the Axioms of Inversion and Product.

Then the classes $A_1$ and $A_2$ exist and so does the function $F\circ G$. $\quad\square$

**Lemma 10.** The function $f:((x,y),z)\mapsto ((x,z),y)$ exists.

*Proof.* Observe that
\begin{multline*}
f=\{(a,b):a,b\in V^3,\;pr_1(a)=pr_1(b), \;pr_2(a)=pr_3(b),\;pr_3(a)=pr_2(b)\}=\\
\{x\in V^3{\times}V^3:pr_1{\circ}p_1(x)=pr_1{\circ}p_2(x),\;
pr_2{\circ}p_1(x)=pr_3{\circ} p_2(x),\;pr_3{\circ} p_1(x)=pr_2{\circ} p_2(x)\}\end{multline*}
and apply Lemmas 3--9. $\quad\square$

Similar arguments can be used to simplify the standard list of Godel's operations (see Definition 13.6 in the book "Set Theory" of Jech):

$G_1(X,Y)=\{X,Y\}$;

$G_2(X,Y)=X\times Y$;

$G_3(X,Y)=\{(x,y)\in X\times Y:x\in y\}$;

$G_4(X,Y)=X\setminus Y$;

$G_5(X,Y)=X\cap Y$;

$G_6(X)=\bigcup X$;

$G_7(X)=dom(X)$;

$G_8(X)=X^{-1}=\{(y,x):(x,y)\in X\}$;

$G_9(X)=\{(u,v,w):(u,w,v)\in X\}$;

$G_{10}(X)=\{(u,v,w):(v,w,u)\in X\}$.

By De Morgan laws, the operation $G_5$ is a composition of the operations $G_1,G_4,G_6$. By Exercise 13.4 in Jech's book, the operation $G_8$ is a composition of the operations $G_2,G_7,G_9,G_{10}$. More precisely, $G_8(X)=dom(G_{10}(G_{10}(G_9(G_{10}(X\times X)))))$. What we already know is that the operation $G_9$ is a composition of the other Godel's operations, so it can be removed (together with $G_5$ from the list, which will reduce to 8 axioms (the same number as was originally in Godel).

It would be interesting to write down the formula expressing the operation $G_9$ via other Godel's operations.

infinitely manytranspositions to generate the group of finitary permutations of $\omega$, hence it is a minor miracle that you can make do with only finitely many axioms at all; it certainly does not give a reason to think that you can reduce the two premutation axioms to one. $\endgroup$ – Emil Jeřábek Apr 8 at 18:34andSeparation as axioms in ZFC because it's easier, and we don't have to go through the proof that Replacement implies Separation. Likewise for Pairing, or Empty Set. $\endgroup$ – Asaf Karagila Apr 9 at 8:35