Definition df-clab 1872

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 1300, which extends or "overloads" the wel 1301 definition connecting set variables, requires that both sides of e. be a class. In df-cleq 1877 and df-clel 1880, 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 1297 allows us to substitute a set variable x for a class variable: all sets are classes by cvjust 1879 (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 1999 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 2346 which is used, for example, to convert elirrv 5700 to elirr 5701.

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 1297	. . 3 class x
3		wph	. . . 4 wff ph
4		vy	. . . 4 set y
5	3, 4	cab 1871	. . 3 class {y | ph}
6	2, 5	wcel 1300	. 2 wff x e. {y | ph}
7	3, 4, 2	wsbc 1534	. 2 wff [x / y]ph
8	6, 7	wb 163	1 wff (x e. {y | ph} <-> [x / y]ph)

This definition is referenced by:  abid 1873  hbab1 1874  hbab 1875  hbabd 1876  cvjust 1879  clelab 2013  vjust 2293  cbvab 2419  sbc8g 2477  sbc8gOLD 2478  sbcel12g 2552  sbceqdig 2554  csbabg 2588  csbabgOLD 2589  difjustOLD 2596  unjustOLD 2599  injustOLD 2602  unab 2859  unabOLD 2860  inab 2861  inabOLD 2862  difab 2863  difabOLD 2864  sbsslemOLD 2979  pwjustOLD 3034  snjustOLD 3048  iinab 3317  brab1 3384  exss 3516  abrexex2 4847  iotaeq 5093  scottexs 5848  scott0s 5849  bnj13 12378  bnj14OLD 12382  bnj35 12404  bnj51 12426  setinds 13844  opabex3 15701  abrexex2g 15738  firnfi3 15743  compne 16417  compab 16418

Copyright terms: Public domain