Description: Define class abstraction
notation (so-called by Quine), also called a
"class builder" in the literature. x and y need not be distinct.
Definition 2.1 of [Quine] p. 16. Typically,
φ will have y as a
free variable, and "{y
∣ φ} " is read "the class of
all sets y
such that φ(y) is true." We do not define {y ∣
φ} 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 1710, which extends or
"overloads" the
wel 1711 definition connecting setvar variables,
requires that both sides of
∈ be a class. In df-cleq 2346 and df-clel 2349, we introduce a new kind
of variable (class variable) that can substituted with expressions such as
{y ∣ φ}. In the present definition, the
x on the left-hand
side is a setvar variable. Syntax definition cv 1641
allows us to substitute
a setvar variable x for
a class variable: all sets are classes by
cvjust 2348 (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 2458 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 done with theorems such as vtoclg 2914 which is used, for
example, to convert elirrv in set.mm to elirr in set.mm.
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 {y ∣ φ} a "class
term".
For a general discussion of the theory of classes, see
https://us.metamath.org/mpeuni/mmset.html#class 2914. (Contributed by NM,
5-Aug-1993.) |