Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-v Structured version   Visualization version   GIF version

Definition df-v 3443
 Description: Define the universal class. Definition 5.20 of [TakeutiZaring] p. 21. Also Definition 2.9 of [Quine] p. 19. The class V can be described as the "class of all sets"; vprc 5183 proves that V is not itself a set in ZFC. We will frequently use the expression 𝐴 ∈ V as a short way to say "𝐴 is a set", and isset 3453 proves that this expression has the same meaning as ∃𝑥𝑥 = 𝐴. The class V is called the "von Neumann universe", however, the letter "V" is not a tribute to the name of von Neumann. The letter "V" was used earlier by Peano in 1889 for the universe of sets, where the letter V is derived from the word "Verum". Peano's notation V was adopted by Whitehead and Russell in Principia Mathematica for the class of all sets in 1910. For a general discussion of the theory of classes, see mmset.html#class 3453. (Contributed by NM, 26-May-1993.)
Assertion
Ref Expression
df-v V = {𝑥𝑥 = 𝑥}

Detailed syntax breakdown of Definition df-v
StepHypRef Expression
1 cvv 3441 . 2 class V
2 vx . . . 4 setvar 𝑥
32, 2weq 1964 . . 3 wff 𝑥 = 𝑥
43, 2cab 2776 . 2 class {𝑥𝑥 = 𝑥}
51, 4wceq 1538 1 wff V = {𝑥𝑥 = 𝑥}
 Colors of variables: wff setvar class This definition is referenced by:  vex  3444  vexOLD  3445  domepOLD  5758  ruv  9050  sa-abvi  30226  elnev  41140
 Copyright terms: Public domain W3C validator