Proof of Class existence theorem (extended version)

Proof

Apply the transformation rules to $\phi$ to produce an equivalent formula containing no relations, special classes, or operations. This formula satisfies the hypothesis of the class existence theorem. Therefore, for all $Y_1, \dots, Y_m,$ there is a unique class $A$ of $n$-tuples satisfying

$$\forall x_1 \cdots \,\forall x_n [(x_1, \dots, x_n) \in A \iff \phi(x_1, \dots, x_n, Y_1, \dots, Y_m)].$$