Definition df-v 3432

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 5253 proves that _V is not itself a set in ZF. We will frequently use the expression A e. _V as a short way to say " A is a set", and isset 3444 proves that this expression has the same meaning as E. x x = A.

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 T. 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 3444. See dfv2 3433 for an alternate definition. (Contributed by NM, 26-May-1993.)

Assertion

Ref	Expression
df-v	|- _V = { x | x = x }

Detailed syntax breakdown of Definition df-v

Step	Hyp	Ref	Expression
1		cvv 3430	. 2 class _V
2		vx	. . . 4 setvar x
3	2, 2	weq 1964	. . 3 wff x = x
4	3, 2	cab 2715	. 2 class { x | x = x }
5	1, 4	wceq 1542	1 wff _V = { x | x = x }

This definition is referenced by:  dfv2  3433  sa-abvi  32532  elnev  44885