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 e. relationship.

This is our first use of the e. symbol to
connect classes instead of
sets. The syntax definition wcel1732, which extends or
"overloads" the
wel1733 definition connecting set variables, requires
that both sides of
e. be a class. In df-cleq2482 and df-clel2485, 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 cv1669
allows us to substitute a
set variable for a class variable: all
sets are classes by cvjust2484
(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 abeq22594 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 vtoclg3070 which is used, for example, to
convert elirrv7732 to elirr7733.

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".