Definition df-clab 2764

Description: Define class abstraction notation (so-called by Quine), also called a "class builder" in the literature. 𝑥 and 𝑦 need not be distinct. Definition 2.1 of [Quine] p. 16. Typically, 𝜑 will have 𝑦 as a free variable, and "{𝑦 ∣ 𝜑} " is read "the class of all sets 𝑦 such that 𝜑(𝑦) is true." We do not define {𝑦 ∣ 𝜑} 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 2107, which extends or "overloads" the wel 2108 definition connecting setvar variables, requires that both sides of ∈ be classes. In df-cleq 2770 and df-clel 2774, we introduce a new kind of variable (class variable) that can be substituted with expressions such as {𝑦 ∣ 𝜑}. In the present definition, the 𝑥 on the left-hand side is a setvar variable. Syntax definition cv 1600 allows us to substitute a setvar variable 𝑥 for a class variable: all sets are classes by cvjust 2772 (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 2892 for a quick overview).

Because class variables can be substituted with compound expressions and setvar variables cannot, it is often useful to convert a theorem containing a free setvar variable to a more general version with a class variable. This is done with theorems such as vtoclg 3467 which is used, for example, to convert elirrv 8792 to elirr 8793.

This is called the "axiom of class comprehension" by [Levy] p. 338, who treats the theory of classes as an extralogical extension to our logic and set theory axioms. He calls the construction {𝑦 ∣ 𝜑} a "class term".

While the three class definitions df-clab 2764, df-cleq 2770, and df-clel 2774 are eliminable and conservative and thus meet the requirements for sound definitions, they are technically axioms in that they do not satisfy the requirements for the current definition checker. The proofs of conservativity require external justification that is beyond the scope of the definition checker.

For a general discussion of the theory of classes, see mmset.html#class. (Contributed by NM, 26-May-1993.)

Assertion

Ref	Expression
df-clab	⊢ (𝑥 ∈ {𝑦 ∣ 𝜑} ↔ [𝑥 / 𝑦]𝜑)

Detailed syntax breakdown of Definition df-clab

Step	Hyp	Ref	Expression
1		vx	. . . 4 setvar 𝑥
2	1	cv 1600	. . 3 class 𝑥
3		wph	. . . 4 wff 𝜑
4		vy	. . . 4 setvar 𝑦
5	3, 4	cab 2763	. . 3 class {𝑦 ∣ 𝜑}
6	2, 5	wcel 2107	. 2 wff 𝑥 ∈ {𝑦 ∣ 𝜑}
7	3, 4, 1	wsb 2011	. 2 wff [𝑥 / 𝑦]𝜑
8	6, 7	wb 198	1 wff (𝑥 ∈ {𝑦 ∣ 𝜑} ↔ [𝑥 / 𝑦]𝜑)

This definition is referenced by:  abid  2765  hbab1  2766  hbab  2768  cvjust  2772  cvjustOLD  2773  abbi2dv  2897  abbilem  2903  abbiiOLD  2909  cbvab  2913  cbvabv  2914  clelab  2916  nfabd  2954  nfabd2OLD  2956  vjust  3399  abv  3408  dfsbcq2  3655  sbc8g  3660  unab  4120  inab  4121  difab  4122  noel  4146  csbab  4234  exss  5165  iotaeq  6109  abrexex2g  7424  opabex3d  7425  opabex3  7426  bj-hbab1  33352  bj-abbi  33356  bj-vjust  33367  eliminable1  33419  bj-cleljustab  33426  bj-vexwt  33427  bj-vexwvt  33429  bj-ab0  33477  bj-snsetex  33527  bj-vjust2  33591  wl-clabv  33969  wl-clabtv  33971  wl-clabt  33972  wl-dfrabv  34000  wl-dfrabf  34002  cleljust2  38126  sn-vexwv  38127  cbvabvw  38142