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.