Definition df-clab 2740

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

3. Remark 1 stresses that df-clab 2740 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 2143). 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 2141 and cab 2739, and it can be called an "extension" of the membership predicate because of wel 2142, whose proof uses cv 1567. An a posteriori justification for cv 1567 is given by cvjust 2755, 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 3742).

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 3521 which is used, for example, to convert elirrv 9558 to elirr 9561.

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

This definition is referenced by:  eleq1ab  2741  abid  2743  vexwt  2744  vexw  2745  nfsab1  2747  hbab  2749  hbabg  2750  cvjust  2755  abbi  2826  abbib  2830  cbvabv  2831  cbvabw  2832  cbvab  2833  eqabbw  2834  eqabdv  2894  clelab  2905  nfaba1  2931  nfabdw  2944  nfabd  2945  rabrabi  3433  abv  3465  abvALT  3466  elab6g  3627  elabgw  3635  elrabi  3645  ralab  3655  dfsbcq2  3746  sbc8g  3751  sbcimdv  3811  sbcg  3815  csbied  3888  dfss2  3922  ss2abim  4013  ss2abdv  4018  unabw  4259  unab  4260  inab  4261  difab  4262  notabw  4265  noel  4290  ab0w  4334  csbab  4404  exss  5444  iotaeq  6504  abrexex2g  7960  opabex3d  7961  opabex3rd  7962  opabex3  7963  scottabf  9865  axregs  35518  xpab  36184  in-ax8  36702  ss-ax8  36703  cbvabdavw  36734  mh-setind  37013  regsfromunir1  37017  bj-dfsbc  37240  eliminable1  37460  eliminable-velab  37466  bj-ab0  37509  bj-elabd2ALT  37527  bj-gabima  37542  bj-snsetex  37565  bj-vn0ALT  37674  wl-df-clab  38116  wl-df.clab  38119  wl-clabv  38205  wl-clabtv  38207  wl-clabt  38208