Is there an already known axiomtization of $NF$ that is **shorter** than the following axiomatic system in first order logic with equality $``="$ and membership $``\in"$? And what is exactly meant by *shorter* is having less total number of symbols in all of its axioms than the total number of symbols in all axioms of this system.

**Extensionality:**as in $NF$**Complements:**$\forall A \exists x \forall y(y \in x \leftrightarrow y \not \in A)$**Pairing:**$ \forall a,b \exists x \forall y(y \in x \leftrightarrow y=a \lor y=b) $**Set union:**$ \forall A \exists x \forall y(y \in x \leftrightarrow \exists m \in A (y \in m)) $**Frege $ 1^*$:**$\exists x \forall y(y \in x \leftrightarrow\exists z \forall m \in y \ (z=m))$**Product:**$\forall R,S \exists x \forall y (y \in x \leftrightarrow \exists r \in R \ \exists s \in S \ \forall z \in y \ ( z \in s \lor z \in r))$**Unordered intersection relation set:**$\exists x \forall y (y \in x \leftrightarrow \exists z \forall m \in y (z \in m))$

The already known finite axiomatizations of $NF$ present in literature that I know of are those of Hailperin and Randall Holmes (see here Pages: 7,15), and those are very long compared to the above mentioned one.