Metamath Proof Explorer

Definition df-v

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 proves that _V is not itself a set in ZFC. We will frequently use the expression A e.V as a short way to say " A is a set", and isset proves that this expression has the same meaning as E. x x = A . 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 . (Contributed by NM, 26-May-1993)

Ref Expression
Assertion df-v V = x | x = x

Detailed syntax breakdown

Step Hyp Ref Expression
0 cvv class V
1 vx setvar x
2 1 cv setvar x
3 2 2 wceq wff x = x
4 3 1 cab class x | x = x
5 0 4 wceq wff V = x | x = x