Definition df-clab 2745

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

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

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

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

This definition is used by:  eleq1ab  2746  abid  2748  vexwt  2749  vexw  2750  nfsab1  2752  hbab  2754  hbabg  2755  cvjust  2760  abbi  2831  abbib  2835  cbvabv  2836  cbvabw  2837  cbvab  2838  eqabbw  2839  eqabdv  2899  clelab  2910  nfaba1  2936  nfabdw  2949  nfabd  2950  rabrabi  3438  abv  3470  abvALT  3471  elab6g  3631  elabgw  3639  elrabi  3649  ralab  3659  dfsbcq2  3750  sbc8g  3755  sbcimdv  3815  sbcg  3819  csbied  3892  dfss2  3926  ss2abim  4017  ss2abdv  4022  unabw  4263  unab  4264  inab  4265  difab  4266  notabw  4269  noel  4294  ab0w  4338  csbab  4408  exss  5447  iotaeq  6508  abrexex2g  7963  opabex3d  7964  opabex3rd  7965  opabex3  7966  scottabf  9870  axregs  35564  xpab  36230  in-ax8  36768  ss-ax8  36769  cbvabdavw  36800  mh-setind  37079  regsfromunir1  37083  bj-dfsbc  37306  eliminable1  37526  eliminable-velab  37532  bj-ab0  37575  bj-elabd2ALT  37593  bj-gabima  37608  bj-snsetex  37631  bj-vn0ALT  37740  wl-df-clab  38182  wl-df.clab  38185  wl-clabv  38271  wl-clabtv  38273  wl-clabt  38274