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 ZF. 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 .

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

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cvv	|- _V
1		vx	|- x
2	1	cv	|- x
3	2 2	wceq	|- x = x
4	3 1	cab	|- { x | x = x }
5	0 4	wceq	|- _V = { x | x = x }