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	$$⊢\mathrm{V}=\left\{x|x=x\right\}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cvv	$$class\mathrm{V}$$
1		vx	$$setvarx$$
2	1	cv	$$setvarx$$
3	2 2	wceq	$$wffx=x$$
4	3 1	cab	$$class\left\{x|x=x\right\}$$
5	0 4	wceq	$$wff\mathrm{V}=\left\{x|x=x\right\}$$