Definition df-clab 1506

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 994, which extends or "overloads" the wel 995 definition connecting set variables, requires that both sides of ∈ be a class. In df-cleq 1511 and df-clel 1514, 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 991 allows us to substitute a set variable x for a class variable: all sets are classes by cvjust 1513 (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 1611 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 1893 which is used, for example, to convert elirrv 4741 to elirr 4742.

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 991	. . 3 class x
3		wph	. . . 4 wff φ
4		vy	. . . 4 set y
5	3, 4	cab 1505	. . 3 class {y∣φ}
6	2, 5	wcel 994	. 2 wff x ∈ {y∣φ}
7	3, 4, 2	wsbc 1207	. 2 wff [x / y]φ
8	6, 7	wb 144	1 wff (x ∈ {y∣φ} ↔ [x / y]φ)

This definition is referenced by:  abid 1507  hbab1 1508  hbab 1509  hbabd 1510  cvjust 1513  clelab 1624  sbc8g 2004  csbabg 2095  unab 2319  inab 2320  difab 2321  exss 2847  abrexex2 3985  scottexs 4864  scott0s 4865  opabex3 11806  abrexex2g 11825  firnfi3 11830

Copyright terms: Public domain