|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.
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
This is our first use of the symbol to connect classes instead of
sets. The syntax definition wcel 1588, which extends or
wel 1589 definition connecting set variables, requires
that both sides of
be a class. In
df-cleq 2134 and df-clel 2137, 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 1585
allows us to substitute a
set variable for a
class variable: all sets are classes by cvjust 2136
(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 2248 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 2588 which is used, for example, to
convert elirrv 5933 to elirr 5934.