Description: Define class abstraction
notation (so-called by Quine), also called a
"class builder" in the literature. and need not be distinct.
Definition 2.1 of [Quine] p. 16.
Typically, will
have as a
free variable, and " " is read "the class of all sets
such that is true." We do not define in
isolation but only as part of an expression that extends or
"overloads"
the
relationship.
This is our first use of the symbol to connect classes instead of
sets. The syntax definition wcel 1721, which extends or
"overloads" the
wel 1722 definition connecting set variables, requires
that both sides of
be a class. In
df-cleq 2397 and df-clel 2400, we introduce a new kind
of variable (class variable) that can substituted with expressions such as
. In
the present definition, the on the left-hand
side is a set variable. Syntax definition cv 1648
allows us to substitute a
set variable for
a class variable: all sets are classes by cvjust 2399
(but not necessarily vice-versa). For a full description of how classes
are introduced and how to recover the primitive language, see the
discussion in Quine (and under abeq2 2509 for a quick overview).
Because class variables can be substituted with compound expressions and
set variables cannot, it is often useful to convert a theorem containing a
free set variable to a more general version with a class variable. This
is done with theorems such as vtoclg 2971 which is used, for example, to
convert elirrv 7521 to elirr 7522.
This is called the "axiom of class comprehension" by [Levy] p. 338, who
treats the theory of classes as an extralogical extension to our logic and
set theory axioms. He calls the construction a "class
term".
For a general discussion of the theory of classes, see
http://us.metamath.org/mpeuni/mmset.html#class.
(Contributed by NM,
5-Aug-1993.) |