---
tag: 9CV112MYW6
kind: statement
role: theorem
name: Class existence theorem
sources:
  - wikipedia: en:528491@r1330985339
    locator: Von Neumann–Bernays–Gödel set theory, section Axiomatization of NBG > Class existence theorem
    note: adopted
    mention: wikipedia://en/528491#3KAG
    sections: [Statement]
inventory: [9YVG4V04HZ]
---

## Statement

Let $\phi(x_1, \dots, x_n, Y_1, \dots, Y_m)$ be a formula that quantifies only over sets and contains no free variables other than $x_1, \dots, x_n, Y_1, \dots, Y_m$ (not necessarily all of these). 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)].$$

The class $A$ is denoted by $\{(x_1, \dots , x_n): \phi(x_1, \dots, x_n, Y_1, \dots, Y_m)\}.$