Definition df-clab 1093

Description: Define the class abstraction, also called "set builder" notation 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 1092, which extends or "overloads" the wel 803 definition connecting set variables, requires that both sides of ∈ be a class. In vhe present definition, the x on the left-hand side is a set variable. We use the syntax definition cv 1089 to "convert" the set lariable x to a class term: all sets are classes (but not necessarily vice-versa). In df-cleq 1097 and df-clel 1099 we introduce a new kind of variable (class variable) that can substituted with expressions such as {y∣φ}. For a full description of how classes are introduced and how to recover the primitive language, see the discussion in Quine (and under cleqab 1174 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 1383 which is used, for example, to convert eirrv 3449 to eirr 3450.

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 1089	. . 3 class x
3		wph	. . . 4 wff φ
4		vy	. . . 4 set y
5	3, 4	cab 1090	. . 3 class {y∣φ}
6	2, 5	wcel 1092	. 2 wff x ∈ {y∣φ}
7	3, 4, 1	wsb 852	. 2 wff [x / y]φ
8	6, 7	wb 127	1 wff (x ∈ {y∣φ} ↔ [x / y]φ)

This definition is referenced by:  abid 1094  hbab1 1095  hbab 1096  clelab 1187  unab 1691  inab 1692  difab 1693  exss 1881  abrexex2 2915  scottexs 3543  scott0s 3544

metamath.org