Let T be a two sorted first order logic with equality, with the first sort written in lower case and it signify elements, while the other sort written in upper case to signify sets. Now we make a restriction on formulation of the language, such that the first sort can only occur on the left of the membership symbol $\in$, and the second sort appear only on the right of it, so for example $X \in Y, x \in y, X \in y$ are all not formulas of the language, we allow the equality sign to occur without restrictions so $X=y, y=X$ are formulas of the language. Now we add a primitive ordered pair $\langle \rangle$ total function on the first sort objects only, meaning that what's inside $\langle \rangle$ must be in lower case for it to be a term expression of the language of this theory.
Axioms of sorting:
Disjoint: $\forall x \forall Y (x \neq Y)$
Existence: $\exists x (x =x)$
Ordered pairs: $\forall x \forall y \exists p (p=\langle x,y \rangle)$
Axioms:
Extensionality: $\forall X,Y (\forall z ( z \in X \leftrightarrow z \in Y) \to X=Y)$
Ordered pairing: $\langle a,b \rangle = \langle c,d \rangle \implies a=c \land b=d$
Comprehension: if $\varphi$ is a formula in which $X$ doesn't occur free; then all closures of: $$\exists X \forall y (y \in X \leftrightarrow \varphi)$$; are axioms.
Question: is T finitely axiomatizable?