Definition df-clab 2741

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

3. Remark 1 stresses that df-clab 2741 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 2147). 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 2145 and cab 2740, and it can be called an "extension" of the membership predicate because of wel 2146, whose proof uses cv 1569. An a posteriori justification for cv 1569 is given by cvjust 2756, 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 3741).

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 9573 to elirr 9576.

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

This definition is used by:  eleq1ab  2742  abid  2744  vexwt  2745  vexw  2746  nfsab1  2748  hbab  2750  hbabg  2751  cvjust  2756  abbi  2827  abbib  2831  cbvabv  2832  cbvabw  2833  cbvab  2834  eqabbw  2835  eqabdv  2895  clelab  2906  nfaba1  2932  nfabdw  2945  nfabd  2946  rabrabi  3433  abv  3465  abvALT  3466  elab6g  3626  elabgw  3634  elrabi  3644  ralab  3654  dfsbcq2  3745  sbc8g  3750  sbcimdv  3810  sbcg  3814  csbied  3886  dfss2  3920  ss2abim  4011  ss2abdv  4016  unabw  4256  unab  4257  inab  4258  difab  4259  notabw  4262  noel  4287  ab0w  4331  csbab  4401  exss  5442  iotaeq  6505  abrexex2g  7965  opabex3d  7966  opabex3rd  7967  opabex3  7968  scottabf  9882  axregs  35673  xpab  36313  in-ax8  36852  ss-ax8  36853  cbvabdavw  36884  mh-setind  37163  regsfromunir1  37167  bj-dfsbc  37390  eliminable1  37610  eliminable-velab  37616  bj-ab0  37659  bj-elabd2ALT  37677  bj-gabima  37692  bj-snsetex  37715  bj-vn0ALT  37824  wl-df-clab  38266  wl-df.clab  38269  wl-clabv  38355  wl-clabtv  38357  wl-clabt  38358