Definition df-clab 2708

Description: Define class abstractions, that is, classes of the form {𝑦 ∣ 𝜑}, which is read "the class of sets 𝑦 such that 𝜑(𝑦)".

A few remarks are in order:

1. The axiomatic statement df-clab 2708 does not define the class abstraction {𝑦 ∣ 𝜑} itself, that is, it does not have the form ⊢ {𝑦 ∣ 𝜑} = ... that a standard definition should have (for a good reason: equality itself has not yet been defined or axiomatized for class abstractions; it is defined later in df-cleq 2721). Instead, df-clab 2708 has the form ⊢ (𝑥 ∈ {𝑦 ∣ 𝜑} ↔ ...), meaning that it only defines what it means for a setvar to be a member of a class abstraction. As a consequence, one can say that df-clab 2708 defines class abstractions if and only if a class abstraction is completely determined by which elements belong to it, which is the content of the axiom of extensionality ax-ext 2701. Therefore, df-clab 2708 can be considered a definition only in systems that can prove ax-ext 2701 (and the necessary first-order logic).

2. As in all definitions, the definiendum (the left-hand side of the biconditional) has no disjoint variable conditions. In particular, the setvar variables 𝑥 and 𝑦 need not be distinct, and the formula 𝜑 may depend on both 𝑥 and 𝑦. This is necessary, as with all definitions, since if there was for instance a disjoint variable condition on 𝑥, 𝑦, then one could not do anything with expressions like 𝑥 ∈ {𝑥 ∣ 𝜑} which are sometimes useful to shorten proofs (because of abid 2711). Most often, however, 𝑥 does not occur in {𝑦 ∣ 𝜑} and 𝑦 is free in 𝜑.

3. Remark 1 stresses that df-clab 2708 does not have the standard form of a definition for a class, but one could be led to think it has the standard form of a definition for a formula. However, it also fails that test since the membership predicate ∈ has already appeared earlier (outside of syntax e.g. in ax-8 2111). Indeed, the definiendum extends, or "overloads", the membership predicate ∈ from formulas of the form "setvar ∈ setvar" to formulas of the form "setvar ∈ class abstraction". This is possible because of wcel 2109 and cab 2707, and it can be called an "extension" of the membership predicate because of wel 2110, whose proof uses cv 1539. An a posteriori justification for cv 1539 is given by cvjust 2723, stating that every setvar can be written as a class abstraction (though conversely not every class abstraction is a set, as illustrated by Russell's paradox ru 3751).

4. Proof techniques. 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 3520 which is used, for example, to convert elirrv 9549 to elirr 9550.

5. Definition or axiom? The question arises with the three axiomatic statements introducing classes, df-clab 2708, df-cleq 2721, and df-clel 2803, to decide if they qualify as definitions or if they should be called axioms. Under the strict definition of "definition" (see conventions 30329), they are not definitions (see Remarks 1 and 3 above, and similarly for df-cleq 2721 and df-clel 2803). One could be less strict and decide to call "definition" every axiomatic statement which provides an eliminable and conservative extension of the considered axiom system. But the notion of conservativity may be given two different meanings in set.mm, due to the difference between the "scheme level" of set.mm and the "object level" of classical treatments. For a proof that these three axiomatic statements yield an eliminable and weakly (that is, object-level) conservative extension of FOL= plus ax-ext 2701, see Appendix of [Levy] p. 357.

6. References and history. The concept of class abstraction dates back to at least Frege, and is used by Whitehead and Russell. This definition is Definition 2.1 of [Quine] p. 16 and Axiom 4.3.1 of [Levy] p. 12. It is called the "axiom of class comprehension" by [Levy] p. 358, who treats the theory of classes as an extralogical extension to predicate logic and set theory axioms. He calls the construction {𝑦 ∣ 𝜑} a "class term". For a full description of how classes are introduced and how to recover the primitive language, see the books of Quine and Levy (and the comment of eqabb 2867 for a quick overview). For a general discussion of the theory of classes, see mmset.html#class 2867. (Contributed by NM, 26-May-1993.) (Revised by BJ, 19-Aug-2023.)

Assertion

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

Detailed syntax breakdown of Definition df-clab

Step	Hyp	Ref	Expression
1		vx	. . . 4 setvar 𝑥
2	1	cv 1539	. . 3 class 𝑥
3		wph	. . . 4 wff 𝜑
4		vy	. . . 4 setvar 𝑦
5	3, 4	cab 2707	. . 3 class {𝑦 ∣ 𝜑}
6	2, 5	wcel 2109	. 2 wff 𝑥 ∈ {𝑦 ∣ 𝜑}
7	3, 4, 1	wsb 2065	. 2 wff [𝑥 / 𝑦]𝜑
8	6, 7	wb 206	1 wff (𝑥 ∈ {𝑦 ∣ 𝜑} ↔ [𝑥 / 𝑦]𝜑)

This definition is referenced by:  eleq1ab  2709  abid  2711  vexwt  2712  vexw  2713  nfsab1  2715  hbab  2717  hbabg  2718  cvjust  2723  abbi  2794  abbib  2798  cbvabv  2799  cbvabw  2800  cbvab  2801  eqabbw  2802  eqabdv  2861  clelab  2873  nfaba1  2899  nfabdw  2913  nfabd  2914  rabrabi  3425  abv  3459  abvALT  3460  elab6g  3635  elabgw  3644  elrabi  3654  ralab  3664  dfsbcq2  3756  sbc8g  3761  sbcimdv  3822  sbcg  3826  csbied  3898  dfss2  3932  ss2abdv  4029  unabw  4270  unab  4271  inab  4272  difab  4273  notabw  4276  noel  4301  vn0  4308  eq0  4313  ab0w  4342  ab0orv  4346  eq0rdv  4370  csbab  4403  disj  4413  rzal  4472  ralf0  4477  exss  5423  iotaeq  6476  abrexex2g  7943  opabex3d  7944  opabex3rd  7945  opabex3  7946  xpab  35713  in-ax8  36212  ss-ax8  36213  cbvabdavw  36244  eliminable1  36847  eliminable-velab  36853  bj-ab0  36896  bj-elabd2ALT  36913  bj-gabima  36928  bj-snsetex  36951  wl-df-clab  37492  wl-clabv  37583  wl-clabtv  37585  wl-clabt  37586  ss2ab1  42207  scottabf  44229