Definition df-clab 2735

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

3. Remark 1 stresses that df-clab 2735 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 2138). 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 2136 and cab 2734, and it can be called an "extension" of the membership predicate because of wel 2137, whose proof uses cv 1553. An a posteriori justification for cv 1553 is given by cvjust 2750, 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 3737).

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 3516 which is used, for example, to convert elirrv 9535 to elirr 9538.

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

This definition is referenced by:  eleq1ab  2736  abid  2738  vexwt  2739  vexw  2740  nfsab1  2742  hbab  2744  hbabg  2745  cvjust  2750  abbi  2821  abbib  2825  cbvabv  2826  cbvabw  2827  cbvab  2828  eqabbw  2829  eqabdv  2889  clelab  2900  nfaba1  2926  nfabdw  2939  nfabd  2940  rabrabi  3427  abv  3460  abvALT  3461  elab6g  3623  elabgw  3631  elrabi  3641  ralab  3650  dfsbcq2  3742  sbc8g  3747  sbcimdv  3807  sbcg  3811  csbied  3883  dfss2  3917  ss2abim  4008  ss2abdv  4013  unabw  4254  unab  4255  inab  4256  difab  4257  notabw  4260  noel  4285  ab0w  4326  csbab  4388  exss  5424  iotaeq  6478  abrexex2g  7934  opabex3d  7935  opabex3rd  7936  opabex3  7937  axregs  35390  xpab  36024  in-ax8  36532  ss-ax8  36533  cbvabdavw  36564  mh-setind  36844  regsfromunir1  36848  bj-dfsbc  37072  eliminable1  37292  eliminable-velab  37298  bj-ab0  37341  bj-elabd2ALT  37358  bj-gabima  37373  bj-snsetex  37396  wl-df-clab  37946  wl-df.clab  37949  wl-clabv  38035  wl-clabtv  38037  wl-clabt  38038  scottabf  44764