MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-clab Structured version   Visualization version   GIF version

Definition df-clab 2800
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 2800 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 2814). Instead, df-clab 2800 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 2800 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 2793. Therefore, df-clab 2800 can be considered a definition only in systems that can prove ax-ext 2793 (and the necessary first-order logic).

2. As in all definitions, the LHS (definiendum) 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 2803). Most often, however, 𝑥 does not occur in {𝑦𝜑} and 𝑦 is free in 𝜑.

3. Remark 1 stresses that df-clab 2800 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 precidate has already appeared earlier (e.g., in the non-syntactic statement ax-8 2107). Indeed, the LHS 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 2105 and cab 2799, and it can be called an "extension" of the membership predicate because of wel 2106, whose proof uses cv 1527. An a posteriori justification for cv 1527 is given by cvjust 2816, 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 3770).

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 3568 which is used, for example, to convert elirrv 9049 to elirr 9050.

5. Definition or axiom? The question arises with the three axiomatic statements introducing classes, df-clab 2800, df-cleq 2814, and df-clel 2893, to decide if they qualify as definitions or if they should be called axioms. Under the strict definition of "definition" (see conventions 28107), they are not definitions (see Remarks 1 and 3 above, and similarly for df-cleq 2814 and df-clel 2893). 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 2793, 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 abeq2 2945 for a quick overview). For a general discussion of the theory of classes, see mmset.html#class 2945. (Contributed by NM, 26-May-1993.) (Revised by BJ, 19-Aug-2023.)

Assertion
Ref Expression
df-clab (𝑥 ∈ {𝑦𝜑} ↔ [𝑥 / 𝑦]𝜑)

Detailed syntax breakdown of Definition df-clab
StepHypRef Expression
1 vx . . . 4 setvar 𝑥
21cv 1527 . . 3 class 𝑥
3 wph . . . 4 wff 𝜑
4 vy . . . 4 setvar 𝑦
53, 4cab 2799 . . 3 class {𝑦𝜑}
62, 5wcel 2105 . 2 wff 𝑥 ∈ {𝑦𝜑}
73, 4, 1wsb 2060 . 2 wff [𝑥 / 𝑦]𝜑
86, 7wb 207 1 wff (𝑥 ∈ {𝑦𝜑} ↔ [𝑥 / 𝑦]𝜑)
Colors of variables: wff setvar class
This definition is referenced by:  eleq1ab  2801  abid  2803  vexwt  2804  vexw  2805  hbab1  2807  nfsab1  2808  hbab  2810  hbabg  2811  cvjust  2816  abbi1  2884  abbi  2888  cbvabv  2889  cbvabw  2890  cbvab  2891  abbi2dv  2950  clelab  2958  nfabdw  3000  nfabd  3001  nfabd2OLD  3003  vjust  3496  abv  3505  dfsbcq2  3774  sbc8g  3779  unab  4269  inab  4270  difab  4271  noel  4295  csbab  4388  exss  5347  iotaeq  6320  abrexex2g  7656  opabex3d  7657  opabex3rd  7658  opabex3  7659  eliminable1  34080  bj-ab0  34122  bj-snsetex  34173  bj-vjust  34241  wl-clabv  34709  wl-clabtv  34711  wl-clabt  34712  wl-dfrabv  34744  wl-dfrabf  34746  scottabf  40456
  Copyright terms: Public domain W3C validator