Definition df-clab 2129

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, 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 1588, which extends or "overloads" the wel 1589 definition connecting set variables, requires that both sides of e. be a class. In df-cleq 2134 and df-clel 2137, we introduce a new kind of variable (class variable) that can substituted with expressions such as {y | ph}. In the present definition, the x on the left-hand side is a set variable. Syntax definition cv 1585 allows us to substitute a set variable x for a class variable: all sets are classes by cvjust 2136 (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 2248 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 2588 which is used, for example, to convert elirrv 5933 to elirr 5934.

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 1585	. . 3 class x
3		wph	. . . 4 wff ph
4		vy	. . . 4 set y
5	3, 4	cab 2128	. . 3 class {y | ph}
6	2, 5	wcel 1588	. 2 wff x e. {y | ph}
7	3, 4, 2	wsbc 1814	. 2 wff [x / y]ph
8	6, 7	wb 219	1 wff (x e. {y | ph} <-> [x / y]ph)

This definition is referenced by:  abid 2130  hbab1 2131  hbab 2132  hbabd 2133  cvjust 2136  clelab 2262  vjust 2539  cbvab 2660  sbc8g 2717  sbcel12g 2785  sbceqg 2786  csbabg 2819  unab 3069  inab 3070  difab 3071  iinab 3487  brab1 3556  exss 3679  reusv2 3972  reusv8OLD 3979  abrexex2g 4932  opabex3 4933  abrexex2 4942  iotaeq 5227  scottexs 6087  scott0s 6088  bnj13 13178  bnj35 13199  bnj51 13214  setinds 14478  opabex3OLD 16525  abrexex2gOLD 16562  firnfi3 16567  compne 17241  compab 17242

Copyright terms: Public domain