| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > df-clab | Structured version Visualization version GIF version | ||
| 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 2714 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 2728). Instead, df-clab 2714 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 2714 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 2707. Therefore, df-clab 2714 can be considered a definition only in systems that can prove ax-ext 2707 (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 2717). Most often, however, 𝑥 does not occur in {𝑦 ∣ 𝜑} and 𝑦 is free in 𝜑. 3. Remark 1 stresses that df-clab 2714 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 2110). 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 2108 and cab 2713, and it can be called an "extension" of the membership predicate because of wel 2109, whose proof uses cv 1539. An a posteriori justification for cv 1539 is given by cvjust 2730, 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 3785). 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 3553 which is used, for example, to convert elirrv 9632 to elirr 9633. 5. Definition or axiom? The question arises with the three axiomatic statements introducing classes, df-clab 2714, df-cleq 2728, and df-clel 2815, to decide if they qualify as definitions or if they should be called axioms. Under the strict definition of "definition" (see conventions 30409), they are not definitions (see Remarks 1 and 3 above, and similarly for df-cleq 2728 and df-clel 2815). 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 2707, 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 2880 for a quick overview). For a general discussion of the theory of classes, see mmset.html#class 2880. (Contributed by NM, 26-May-1993.) (Revised by BJ, 19-Aug-2023.) |
| Ref | Expression |
|---|---|
| df-clab | ⊢ (𝑥 ∈ {𝑦 ∣ 𝜑} ↔ [𝑥 / 𝑦]𝜑) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | vx | . . . 4 setvar 𝑥 | |
| 2 | 1 | cv 1539 | . . 3 class 𝑥 |
| 3 | wph | . . . 4 wff 𝜑 | |
| 4 | vy | . . . 4 setvar 𝑦 | |
| 5 | 3, 4 | cab 2713 | . . 3 class {𝑦 ∣ 𝜑} |
| 6 | 2, 5 | wcel 2108 | . 2 wff 𝑥 ∈ {𝑦 ∣ 𝜑} |
| 7 | 3, 4, 1 | wsb 2064 | . 2 wff [𝑥 / 𝑦]𝜑 |
| 8 | 6, 7 | wb 206 | 1 wff (𝑥 ∈ {𝑦 ∣ 𝜑} ↔ [𝑥 / 𝑦]𝜑) |
| Colors of variables: wff setvar class |
| This definition is referenced by: eleq1ab 2715 abid 2717 vexwt 2718 vexw 2719 nfsab1 2721 hbab1OLD 2723 hbab 2724 hbabg 2725 cvjust 2730 abbi 2806 abbib 2810 cbvabv 2811 cbvabw 2812 cbvab 2813 eqabbw 2814 eqabdv 2874 clelab 2886 nfaba1 2912 nfabdw 2926 nfabd 2927 rabrabi 3455 abv 3491 abvALT 3492 elab6g 3668 elabgw 3676 elrabi 3686 ralab 3696 dfsbcq2 3790 sbc8g 3795 sbcimdv 3858 sbcg 3862 csbied 3934 dfss2 3968 ss2abdv 4065 unabw 4306 unab 4307 inab 4308 difab 4309 notabw 4312 noel 4337 vn0 4344 eq0 4349 ab0w 4378 ab0orv 4382 eq0rdv 4406 csbab 4439 disj 4449 rzal 4508 ralf0 4513 exss 5466 iotaeq 6524 abrexex2g 7985 opabex3d 7986 opabex3rd 7987 opabex3 7988 xpab 35719 in-ax8 36218 ss-ax8 36219 cbvabdavw 36250 eliminable1 36853 eliminable-velab 36859 bj-ab0 36902 bj-elabd2ALT 36919 bj-gabima 36934 bj-snsetex 36957 wl-df-clab 37498 wl-clabv 37589 wl-clabtv 37591 wl-clabt 37592 ss2ab1 42251 scottabf 44252 |
| Copyright terms: Public domain | W3C validator |