![]() |
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 2704 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 2718). Instead, df-clab 2704 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 2704 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 2697. Therefore, df-clab 2704 can be considered a definition only in systems that can prove ax-ext 2697 (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 2707). Most often, however, 𝑥 does not occur in {𝑦 ∣ 𝜑} and 𝑦 is free in 𝜑. 3. Remark 1 stresses that df-clab 2704 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 2100). 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 2098 and cab 2703, and it can be called an "extension" of the membership predicate because of wel 2099, whose proof uses cv 1532. An a posteriori justification for cv 1532 is given by cvjust 2720, 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 3771). 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 3537 which is used, for example, to convert elirrv 9590 to elirr 9591. 5. Definition or axiom? The question arises with the three axiomatic statements introducing classes, df-clab 2704, df-cleq 2718, and df-clel 2804, to decide if they qualify as definitions or if they should be called axioms. Under the strict definition of "definition" (see conventions 30157), they are not definitions (see Remarks 1 and 3 above, and similarly for df-cleq 2718 and df-clel 2804). 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 2697, 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 2867 for a quick overview). For a general discussion of the theory of classes, see mmset.html#class 2867. (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 1532 | . . 3 class 𝑥 |
3 | wph | . . . 4 wff 𝜑 | |
4 | vy | . . . 4 setvar 𝑦 | |
5 | 3, 4 | cab 2703 | . . 3 class {𝑦 ∣ 𝜑} |
6 | 2, 5 | wcel 2098 | . 2 wff 𝑥 ∈ {𝑦 ∣ 𝜑} |
7 | 3, 4, 1 | wsb 2059 | . 2 wff [𝑥 / 𝑦]𝜑 |
8 | 6, 7 | wb 205 | 1 wff (𝑥 ∈ {𝑦 ∣ 𝜑} ↔ [𝑥 / 𝑦]𝜑) |
Colors of variables: wff setvar class |
This definition is referenced by: eleq1ab 2705 abid 2707 vexwt 2708 vexw 2709 nfsab1 2711 hbab1OLD 2713 hbab 2714 hbabg 2715 cvjust 2720 abbi 2794 abbib 2798 cbvabv 2799 cbvabw 2800 cbvabwOLD 2801 cbvab 2802 eqabbw 2803 eqabdv 2861 clelab 2873 clelabOLD 2874 nfabdw 2920 nfabdwOLD 2921 nfabd 2922 rabrabi 3444 abv 3479 abvALT 3480 elab6g 3654 elrabi 3672 ralab 3682 dfsbcq2 3775 sbc8g 3780 sbcimdv 3846 sbcg 3851 csbied 3926 ss2abdv 4055 ss2abdvALT 4056 unabw 4292 unab 4293 inab 4294 difab 4295 notabw 4298 noel 4325 noelOLD 4326 vn0 4333 eq0 4338 ab0w 4368 ab0OLD 4370 ab0orv 4373 eq0rdv 4399 csbab 4432 disj 4442 rzal 4503 ralf0 4508 exss 5456 iotaeq 6501 abrexex2g 7947 opabex3d 7948 opabex3rd 7949 opabex3 7950 xpab 35228 eliminable1 36244 eliminable-velab 36250 bj-ab0 36294 bj-elabd2ALT 36311 bj-gabima 36326 bj-snsetex 36350 wl-clabv 36969 wl-clabtv 36971 wl-clabt 36972 ss2ab1 41579 elabgw 41968 scottabf 43557 |
Copyright terms: Public domain | W3C validator |