Short Axiomatization of Stratified Comprehension

There are several finite axiomatizations of stratified comprehension. The famous two are Hailperin's and Randall Holmes's. However, the system presented here could be the shortest known one written in the first order language of set theory. This axiomatization uses unordered pairs, unlike the prior axiomaizations which used ordered pairs, so this makes a simpler formulation in the first order language of set theory. The proof works under absence of Extensionality, so it can serve to complete an axiomatization of NFU or NF.