---
tag: P8WRV9X978
kind: statement
role: theorem
name: Class existence theorem (extended version)
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#2D64
    sections: [Statement]
inventory: [58V2GWSYTJ]
---

## Statement

Let $\phi(x_1, \dots, x_n, Y_1, \dots, Y_m)$ be a formula that quantifies only over sets, contains no free variables other than $x_1, \dots, x_n, Y_1, \dots, Y_m$, and may contain relations, special classes, and operations defined by formulas that quantify only over sets. Then for all $Y_1, \dots, Y_m,$ there exists a unique class $A$ of $n$-tuples such that

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