Definition df-clab 1457

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 955, which extends or "overloads" the wel 956 definition connecting set variables, requires that both sides of ∈ be a class. In df-cleq 1462 and df-clel 1465, 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 set variable. Syntax definition cv 952 allows us to substitute a set variable x for a class variable: all sets are classes by cvjust 1464 (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 1560 for a quick overview).

Because class variables can be substituted with compound expressions and set variables cannot, it is often useful to convert a theorem containing a free set variable to a more general version with a class variable. This is done with theorems such as vtoclg 1838 which is used, for example, to convert elirrv 4570 to elirr 4571.

Assertion

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

Detailed syntax breakdown of Definition df-clab

Step	Hyp	Ref	Expression
1		vx	. . . 4 set x
2	1	cv 952	. . 3 class x
3		wph	. . . 4 wff φ
4		vy	. . . 4 set y
5	3, 4	cab 1456	. . 3 class {y∣φ}
6	2, 5	wcel 955	. 2 wff x ∈ {y∣φ}
7	3, 4, 2	wsbc 1166	. 2 wff [x / y]φ
8	6, 7	wb 146	1 wff (x ∈ {y∣φ} ↔ [x / y]φ)

This definition is referenced by:  abid 1458  hbab1 1459  hbab 1460  hbabd 1461  cvjust 1464  clelab 1573  csbabg 2033  unab 2257  inab 2258  difab 2259  exss 2759  abrexex2 3856  scottexs 4690  scott0s 4691

Copyright terms: Public domain