A little a head of ZF

This theory is based on the same hierarchical intuition behind that of ZF, yet it is indeed much stronger than ZF:

This question is about a certain technical issue about defining recursions, the question here is about if pairing is indispensable here, the theory is written in first order logic with equality and membership.

Axioms: ID axioms +

Extensionality: ∀z(z∈A↔z∈B)→A=B∀z(z∈A↔z∈B)→A=B

Define: set(y)⟺∃z (y∈z)set(y)⟺∃z (y∈z)

Class Comprehension: [∃X∀y(y∈X↔set(y)∧ϕ(y))][∃X∀y(y∈X↔set(y)∧ϕ(y))], for every formula ϕ(y)ϕ(y) in which XX is not free.

Define: X=V⟺∀y(set(y)→y∈X)X=V⟺∀y(set(y)→y∈X)

Pairing: ∀x,y∈V:{x,y}∈V∀x,y∈V:{x,y}∈V

Define: Stage(X)⟺∃α:ordinal(α)∧X=VαStage(X)⟺∃α:ordinal(α)∧X=Vα

Where: Vα={x⊆Vβ:β<α}Vα={x⊆Vβ:β<α}

In order to show that this can be written in the language of this theory, the exact formal expression is a bit long, that is:

X=Vα⟺∃Y:∀m∈Y∃β<α(β=I(m))∧∀β<α∃z∈Y(I(z)=β)∧∀k∈Y(I(k)=∅→k=∅)∧∀a,b∈Y(I(b)=I(a)+1→b=P(a))∧∀c∈Y(lim(I(c))→c=⋃{d∈Y:I(d)<I(c)})∧X={w⊆t:t∈Y}X=Vα⟺∃Y:∀m∈Y∃β<α(β=I(m))∧∀β<α∃z∈Y(I(z)=β)∧∀k∈Y(I(k)=∅→k=∅)∧∀a,b∈Y(I(b)=I(a)+1→b=P(a))∧∀c∈Y(lim(I(c))→c=⋃{d∈Y:I(d)<I(c)})∧X={w⊆t:t∈Y}

Where: I(x)I(x) stands for the "index of x", defined as:

Foundation: ∀x∈V∃Y:Stage(Y)∧x∈Y∀x∈V∃Y:Stage(Y)∧x∈Y

A stage VαVα is said to be reachable from below if and only if it is empty or there exists a class XX of prior stages that is strictly subnumerous to VαVα such that VαVα is subnumrous to P(⋃X)P(⋃X)

Where: X subnumerous to Y ⟺X⊆Y∨∃f:X↪YX subnumerous to Y ⟺X⊆Y∨∃f:X↪Y

A stage VαVα is said to be weakly reachable from ∅∅ if and only if it is empty or the class of all prior stages that are not reachable from below is strictly subnumerous to it.

Reachability: Vα is weakly reachable from ∅∧X⊆Vα→X∈VVα is weakly reachable from ∅∧X⊆Vα→X∈V

This theory is stronger than ZF. I think it entails the existence of an inaccessible proper class of inaccessible stages, more specifically: A Grothendieck universe that is the union of a proper class of Grothendieck universes.

Is it possible to drop pairing from the above theory?

The degree of weak reachability of a stage VαVα from ∅∅ can be defined as the cardinality of the class of all prior stages that are not reachable from below. It can be seen that sets of ZF are those belonging to stages that are ≤1≤1 degree weakly reachable from the empty set. While the sets in TG set theory are those belonging to stages that are <ℵ0<ℵ0 degree weakly reachable from the empty set. This theory is vastly huger than those levels. It can be seen as a theory involved with the lower tiers of large cardinals, and moreover its a straightforward offshoot of the notion of a hierarchy, so it does have the same underlying motivation of ZF, but pushes it further into larger sets.

You can see this theory at: 

axioms - Is pairing required for defining stages of the cumulative hierarchy in this class theory? - Mathematics Stack Exchange