# Metamath Proof Explorer

## 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 ${setvar}{x}$
2 1 cv ${setvar}{x}$
3 2 2 wceq ${wff}{x}={x}$
4 3 1 cab ${class}\left\{{x}|{x}={x}\right\}$
5 0 4 wceq ${wff}\mathrm{V}=\left\{{x}|{x}={x}\right\}$