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.

differentfrom known axioms/descriptions can express a deep truth about $K$, and can help understand $K$ better. Finding one that is merelyshorterseems less helpful/interesting to me. When comparing two axiom systems of humanly readable length for $K$, the shorter one will often be more difficult to understand. (Not always, though; the axiom system {"false"} is very easily understood, but I will not claim that it is equivalent to NF.) $\endgroup$ – Goldstern Oct 19 '19 at 12:51