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 1448, which extends or
"overloads" the
wel 1449 definition connecting setvar variables,
requires that both sides of
be a class. In
df-cleq 2093 and df-clel 2096, 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 setvar variable. Syntax definition cv 1298
allows us to substitute
a setvar variable
for a class variable: all sets are classes by
cvjust 2095 (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 2208 for a quick overview).
Because class variables can be substituted with compound expressions and
setvar variables cannot, it is often useful to convert a theorem
containing a free setvar variable to a more general version with a class
variable.
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
https://us.metamath.org/mpeuni/mmset.html#class.
(Contributed by NM,
5-Aug-1993.) |