Description: Every set is a class. Proposition 4.9 of TakeutiZaring p. 13. This
theorem shows that a setvar variable can be expressed as a class
abstraction. This provides a motivation for the class syntax
construction cv , which allows us to substitute a setvar variable for
a class variable. See also cab and df-clab . Note that this is not
a rigorous justification, because cv is used as part of the proof of
this theorem, but a careful argument can be made outside of the
formalism of Metamath, for example as is done in Chapter 4 of Takeuti
and Zaring. See also the discussion under the definition of class in
Jech p. 4 showing that "Every set can be considered to be a class."
See abid1 for the version of cvjust extended to classes.
(Contributed by NM, 7-Nov-2006) Avoid ax-13 . (Revised by Wolf
Lammen, 4-May-2023)