Definition df-clab 2742

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

3. Remark 1 stresses that df-clab 2742 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 2149). 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 2147 and cab 2741, and it can be called an "extension" of the membership predicate because of wel 2148, whose proof uses cv 1569. An a posteriori justification for cv 1569 is given by cvjust 2757, 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 3521 which is used, for example, to convert elirrv 9618 to elirr 9621.

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

This definition is used by:  eleq1ab  2743  abid  2745  vexwt  2746  vexw  2747  nfsab1  2749  hbab  2751  hbabg  2752  cvjust  2757  abbi  2828  abbib  2832  abbibOLD  2833  cbvabv  2834  cbvabw  2835  cbvab  2836  eqabbw  2837  eqabdv  2897  clelab  2908  nfaba1  2934  nfabdw  2947  nfabd  2948  rabrabi  3434  abv  3466  abvALT  3467  elab6g  3626  elabgw  3634  elrabi  3644  ralab  3654  dfsbcq2  3745  sbc8g  3750  sbcimdv  3810  sbcg  3814  csbied  3887  ss2abim  3988  ss2abdv  3993  dfss2  4097  unabw  4255  unab  4256  inab  4257  difab  4258  notabw  4261  noel  4286  noelOLD  4287  ab0w  4331  csbab  4401  exss  5435  iotaeq  6524  abrexex2g  8000  opabex3d  8001  opabex3rd  8002  opabex3  8003  scottabf  9966  axregs  35907  xpab  36669  in-ax8  37191  ss-ax8  37192  cbvabdavw  37223  mh-setind  37502  regsfromunir1  37506  bj-dfsbc  37729  eliminable1  37949  eliminable-velab  37955  bj-ab0  37998  bj-elabd2ALT  38016  bj-gabima  38031  bj-snsetex  38054  bj-vn0ALT  38178  wl-df-clab  38619  wl-df.clab  38622  wl-clabv  38708  wl-clabtv  38710  wl-clabt  38711