---
tag: 3FN40MMTBF
kind: proof
name: Proof of Class existence theorem (extended version)
proves: P8WRV9X978
sources:
  - wikipedia: en:528491@r1330985339
    locator: Von Neumann–Bernays–Gödel set theory, section Axiomatization of NBG > Extending the class existence theorem
    note: adopted
    mention: wikipedia://en/528491#KXUY
    sections: [Proof]
---

## 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)].$$