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