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

Definition df-v 3468
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 5306 proves that V is not itself a set in ZF. We will frequently use the expression 𝐴 ∈ V as a short way to say "𝐴 is a set", and isset 3479 proves that this expression has the same meaning as 𝑥𝑥 = 𝐴.

In well-founded set theories without urelements, like ZF, the class V is equal to the von Neumann universe. However, the letter "V" does not stand for "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 Latin word "Verum", referring to the true truth constant 𝑇. Peano's notation V was adopted by Whitehead and Russell in Principia Mathematica for the class of all sets in 1910.

The class constant V is the first class constant introduced in this database. As a constant, as opposed to a variable, it cannot be substituted with anything, and in particular it is not part of any disjoint variable condition.

For a general discussion of the theory of classes, see mmset.html#class 3479. See dfv2 3469 for an alternate definition. (Contributed by NM, 26-May-1993.)

Assertion
Ref Expression
df-v V = {𝑥𝑥 = 𝑥}

Detailed syntax breakdown of Definition df-v
StepHypRef Expression
1 cvv 3466 . 2 class V
2 vx . . . 4 setvar 𝑥
32, 2weq 1958 . . 3 wff 𝑥 = 𝑥
43, 2cab 2701 . 2 class {𝑥𝑥 = 𝑥}
51, 4wceq 1533 1 wff V = {𝑥𝑥 = 𝑥}
Colors of variables: wff setvar class
This definition is referenced by:  dfv2  3469  vexOLD  3471  sa-abvi  32168  elnev  43711
  Copyright terms: Public domain W3C validator