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)