Definition df-clab 2183

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 2167, which extends or "overloads" the wel 2168 definition connecting setvar variables, requires that both sides of ∈ be a class. In df-cleq 2189 and df-clel 2192, 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 1363 allows us to substitute a setvar variable 𝑥 for a class variable: all sets are classes by cvjust 2191 (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 2305 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 2305. (Contributed by NM, 5-Aug-1993.)

Assertion

Ref	Expression
df-clab	⊢ (𝑥 ∈ {𝑦 ∣ 𝜑} ↔ [𝑥 / 𝑦]𝜑)

Detailed syntax breakdown of Definition df-clab

Step	Hyp	Ref	Expression
1		vx	. . . 4 setvar 𝑥
2	1	cv 1363	. . 3 class 𝑥
3		wph	. . . 4 wff 𝜑
4		vy	. . . 4 setvar 𝑦
5	3, 4	cab 2182	. . 3 class {𝑦 ∣ 𝜑}
6	2, 5	wcel 2167	. 2 wff 𝑥 ∈ {𝑦 ∣ 𝜑}
7	3, 4, 1	wsb 1776	. 2 wff [𝑥 / 𝑦]𝜑
8	6, 7	wb 105	1 wff (𝑥 ∈ {𝑦 ∣ 𝜑} ↔ [𝑥 / 𝑦]𝜑)

This definition is referenced by:  abid  2184  hbab1  2185  hbab  2187  cvjust  2191  abbi  2310  sb8ab  2318  cbvabw  2319  cbvab  2320  clelab  2322  eqabdv  2325  nfabdw  2358  nfabd  2359  vjust  2764  dfsbcq2  2992  sbc8g  2997  csbcow  3095  csbabg  3146  unab  3430  inab  3431  difab  3432  rabeq0  3480  abeq0  3481  oprcl  3832  exss  4260  peano1  4630  peano2  4631  iotaeq  5227  nfvres  5592  abrexex2g  6177  opabex3d  6178  opabex3  6179  abrexex2  6181  bdab  15484  bdph  15496  bdcriota  15529