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, ph will have y as a free variable, and "{y | ph}" is read "the class of all sets y such that ph(y) is true." We do not define {y | ph} in isolation but only as part of an expression that extends or "overloads" the e. relationship.

This is our first use of the e. 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 e. be a class. In the present definition, the x on the left-hand side is a set variable. We use the syntax definition cv 1089 to "convert" the set variable 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 | ph}. 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 e. {y | ph} <-> [x / y]ph)

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

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