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

Definition df-v 3008
Description: Define the universal class. Definition 5.20 of [TakeutiZaring] p. 21. Also Definition 2.9 of [Quine] p. 19. The class can be described as the "class of all sets"; vprc 4440 proves that is not itself a set in ZFC. We will frequently use the expression as a short way to say " is a set", and isset 3010 proves that this expression has the same meaning as . The class 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 http://us.metamath.org/mpeuni/mmset.html#class. (Contributed by NM, 5-Aug-1993.)
Assertion
Ref Expression
df-v

Detailed syntax breakdown of Definition df-v
StepHypRef Expression
1 cvv 3006 . 2
2 vx . . . 4
32, 2weq 1663 . . 3
43, 2cab 2467 . 2
51, 4wceq 1662 1
Colors of variables: wff set class
This definition is referenced by:  vex  3009  int0  4152  ruv  7680  foo3  24457  domep  26250  elnev  28541
  Copyright terms: Public domain W3C validator