Definition df-clab 2706

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

3. Remark 1 stresses that df-clab 2706 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 2100). 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 2098 and cab 2705, and it can be called an "extension" of the membership predicate because of wel 2099, whose proof uses cv 1532. An a posteriori justification for cv 1532 is given by cvjust 2722, 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 3777).

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 3542 which is used, for example, to convert elirrv 9627 to elirr 9628.

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

This definition is referenced by:  eleq1ab  2707  abid  2709  vexwt  2710  vexw  2711  nfsab1  2713  hbab1OLD  2715  hbab  2716  hbabg  2717  cvjust  2722  abbi  2796  abbib  2800  cbvabv  2801  cbvabw  2802  cbvabwOLD  2803  cbvab  2804  eqabbw  2805  eqabdv  2863  clelab  2875  clelabOLD  2876  nfaba1  2907  nfabdw  2923  nfabdwOLD  2924  nfabd  2925  rabrabi  3449  abv  3484  abvALT  3485  elab6g  3659  elrabi  3678  ralab  3688  dfsbcq2  3781  sbc8g  3786  sbcimdv  3852  sbcg  3857  csbied  3932  ss2abdv  4060  ss2abdvALT  4061  unabw  4300  unab  4301  inab  4302  difab  4303  notabw  4306  noel  4334  noelOLD  4335  vn0  4342  eq0  4347  ab0w  4377  ab0OLD  4379  ab0orv  4382  eq0rdv  4408  csbab  4441  disj  4451  rzal  4512  ralf0  4517  exss  5469  iotaeq  6518  abrexex2g  7974  opabex3d  7975  opabex3rd  7976  opabex3  7977  xpab  35353  eliminable1  36369  eliminable-velab  36375  bj-ab0  36419  bj-elabd2ALT  36436  bj-gabima  36451  bj-snsetex  36475  wl-clabv  37095  wl-clabtv  37097  wl-clabt  37098  ss2ab1  41738  elabgw  42121  scottabf  43708