Definition df-clab 2024

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 1390, which extends or "overloads" the wel 1391 definition connecting setvar variables, requires that both sides of ∈ be a class. In df-cleq 2030 and df-clel 2033, 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 1241 allows us to substitute a setvar variable x for a class variable: all sets are classes by cvjust 2032 (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 2143 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.)

Assertion

Ref	Expression
df-clab	⊢ (x ∈ {y ∣ φ} ↔ [x / y]φ)

Detailed syntax breakdown of Definition df-clab

Step	Hyp	Ref	Expression
1		vx	. . . 4 setvar x
2	1	cv 1241	. . 3 class x
3		wph	. . . 4 wff φ
4		vy	. . . 4 setvar y
5	3, 4	cab 2023	. . 3 class {y ∣ φ}
6	2, 5	wcel 1390	. 2 wff x ∈ {y ∣ φ}
7	3, 4, 1	wsb 1642	. 2 wff [x / y]φ
8	6, 7	wb 98	1 wff (x ∈ {y ∣ φ} ↔ [x / y]φ)

This definition is referenced by:  abid  2025  hbab1  2026  hbab  2028  cvjust  2032  abbi  2148  sb8ab  2156  cbvab  2157  clelab  2159  nfabd  2193  vjust  2552  dfsbcq2  2761  sbc8g  2765  csbabg  2901  unab  3198  inab  3199  difab  3200  rabeq0  3241  abeq0  3242  oprcl  3564  exss  3954  peano1  4260  peano2  4261  iotaeq  4818  nfvres  5149  abrexex2g  5689  opabex3d  5690  opabex3  5691  abrexex2  5693  bdab  9293  bdph  9305  bdcriota  9338