Math 2.0

Theorem

Class existence theorem (extended version)

Statement

Let ϕ(x1,…,xn,Y1,…,Ym)\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 x1,…,xn,Y1,…,Ymx_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 Y1,…,Ym,Y_1, \dots, Y_m, there exists a unique class AA of nn-tuples such that

∀x1⋯ ∀xn[(x1,…,xn)∈A  ⟺  ϕ(x1,…,xn,Y1,…,Ym)].\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)].

Reading path

To understand this page from the ground up, read these 2 pages in order. The foundations come first. The path takes the proof Proof of Class existence theorem (extended version).

Show the path as a graph
Proof of Class existence theorem (extended version), proof, no evidence levelProof of Class existe…proofClass existence theorem (extended version), statement, no evidence levelClass existence theor…statement
Each page uses the pages above it. The colour of the bar on a box shows how strong the evidence is, and the box also gives it as text. The list has the same pages.
  • no evidence level
  1. Proof of Class existence theorem (extended version) proof
  2. Class existence theorem (extended version) statement

Further reading

  1. Wikipedia, page 528491, revision 1330985339, Von Neumann–Bernays–Gödel set theory, section Axiomatization of NBG > Extending the class existence theorem. adopted
About this page
TagP8WRV9X978
URIm2://P8WRV9X978
Kindstatement, theorem
WritingW0 stub
StatusThis copy of the site has no build data. Run m2 status P8WRV9X978.
Changed4 November 2026

Markdown · JSON · Edit on GitHub

What this page needs for W1

  • edge uses out: each definition that the statement needs (0 of 1)

The writing levels say how complete the text of a page is. They do not measure its truth.

What links here

Proofs