Definition df-clab 2718

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 2718 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 2732). Instead, df-clab 2718 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 2718 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 2711. Therefore, df-clab 2718 can be considered a definition only in systems that can prove ax-ext 2711 (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 2721). Most often, however, 𝑥 does not occur in {𝑦 ∣ 𝜑} and 𝑦 is free in 𝜑.

3. Remark 1 stresses that df-clab 2718 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 2110). 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 2108 and cab 2717, and it can be called an "extension" of the membership predicate because of wel 2109, whose proof uses cv 1536. An a posteriori justification for cv 1536 is given by cvjust 2734, 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 3802).

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 3566 which is used, for example, to convert elirrv 9665 to elirr 9666.

5. Definition or axiom? The question arises with the three axiomatic statements introducing classes, df-clab 2718, df-cleq 2732, and df-clel 2819, to decide if they qualify as definitions or if they should be called axioms. Under the strict definition of "definition" (see conventions 30432), they are not definitions (see Remarks 1 and 3 above, and similarly for df-cleq 2732 and df-clel 2819). 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 2711, 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 2884 for a quick overview). For a general discussion of the theory of classes, see mmset.html#class 2884. (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 1536	. . 3 class 𝑥
3		wph	. . . 4 wff 𝜑
4		vy	. . . 4 setvar 𝑦
5	3, 4	cab 2717	. . 3 class {𝑦 ∣ 𝜑}
6	2, 5	wcel 2108	. 2 wff 𝑥 ∈ {𝑦 ∣ 𝜑}
7	3, 4, 1	wsb 2064	. 2 wff [𝑥 / 𝑦]𝜑
8	6, 7	wb 206	1 wff (𝑥 ∈ {𝑦 ∣ 𝜑} ↔ [𝑥 / 𝑦]𝜑)

This definition is referenced by:  eleq1ab  2719  abid  2721  vexwt  2722  vexw  2723  nfsab1  2725  hbab1OLD  2727  hbab  2728  hbabg  2729  cvjust  2734  abbi  2810  abbib  2814  cbvabv  2815  cbvabw  2816  cbvab  2817  eqabbw  2818  eqabdv  2878  clelab  2890  nfaba1  2916  nfabdw  2932  nfabdwOLD  2933  nfabd  2934  rabrabi  3463  abv  3500  abvALT  3501  elab6g  3682  elabgw  3692  elrabi  3703  ralab  3713  dfsbcq2  3807  sbc8g  3812  sbcimdv  3878  sbcg  3883  csbied  3959  dfss2  3994  ss2abdv  4089  unabw  4326  unab  4327  inab  4328  difab  4329  notabw  4332  noel  4360  noelOLD  4361  vn0  4368  eq0  4373  ab0w  4401  ab0OLD  4403  ab0orv  4406  eq0rdv  4430  csbab  4463  disj  4473  rzal  4532  ralf0  4537  exss  5483  iotaeq  6538  abrexex2g  8005  opabex3d  8006  opabex3rd  8007  opabex3  8008  xpab  35688  in-ax8  36190  ss-ax8  36191  cbvabdavw  36222  eliminable1  36825  eliminable-velab  36831  bj-ab0  36874  bj-elabd2ALT  36891  bj-gabima  36906  bj-snsetex  36929  wl-clabv  37549  wl-clabtv  37551  wl-clabt  37552  ss2ab1  42212  scottabf  44209