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 1374, which extends or
"overloads" the
wel 1375 definition connecting setvar variables,
requires that both sides of
∈ be a class.
In df-cleq 2015 and df-clel 2018, 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 1227
allows us to substitute
a setvar variable x for a class variable: all sets are classes
by
cvjust 2017 (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 2128 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 {y ∣ φ} 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.) |