![]() |
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 2711 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 2725). Instead, df-clab 2711 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 2711 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 2704. Therefore, df-clab 2711 can be considered a definition only in systems that can prove ax-ext 2704 (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 2714). Most often, however, 𝑥 does not occur in {𝑦 ∣ 𝜑} and 𝑦 is free in 𝜑. 3. Remark 1 stresses that df-clab 2711 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 (e.g., in the non-syntactic statement ax-8 2109). 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 2107 and cab 2710, and it can be called an "extension" of the membership predicate because of wel 2108, whose proof uses cv 1541. An a posteriori justification for cv 1541 is given by cvjust 2727, 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 3775). 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 3556 which is used, for example, to convert elirrv 9587 to elirr 9588. 5. Definition or axiom? The question arises with the three axiomatic statements introducing classes, df-clab 2711, df-cleq 2725, and df-clel 2811, to decide if they qualify as definitions or if they should be called axioms. Under the strict definition of "definition" (see conventions 29633), they are not definitions (see Remarks 1 and 3 above, and similarly for df-cleq 2725 and df-clel 2811). 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 2704, 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 2874 for a quick overview). For a general discussion of the theory of classes, see mmset.html#class 2874. (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 1541 | . . 3 class 𝑥 |
3 | wph | . . . 4 wff 𝜑 | |
4 | vy | . . . 4 setvar 𝑦 | |
5 | 3, 4 | cab 2710 | . . 3 class {𝑦 ∣ 𝜑} |
6 | 2, 5 | wcel 2107 | . 2 wff 𝑥 ∈ {𝑦 ∣ 𝜑} |
7 | 3, 4, 1 | wsb 2068 | . 2 wff [𝑥 / 𝑦]𝜑 |
8 | 6, 7 | wb 205 | 1 wff (𝑥 ∈ {𝑦 ∣ 𝜑} ↔ [𝑥 / 𝑦]𝜑) |
Colors of variables: wff setvar class |
This definition is referenced by: eleq1ab 2712 abid 2714 vexwt 2715 vexw 2716 nfsab1 2718 hbab1OLD 2720 hbab 2721 hbabg 2722 cvjust 2727 abbi 2801 abbib 2805 cbvabv 2806 cbvabw 2807 cbvabwOLD 2808 cbvab 2809 eqabbw 2810 eqabdv 2868 clelab 2880 clelabOLD 2881 nfabdw 2927 nfabdwOLD 2928 nfabd 2929 rabrabi 3451 abv 3486 abvALT 3487 elab6g 3658 elrabi 3676 ralab 3686 dfsbcq2 3779 sbc8g 3784 sbcimdv 3850 sbcg 3855 csbied 3930 ss2abdv 4059 ss2abdvALT 4060 unabw 4296 unab 4297 inab 4298 difab 4299 notabw 4302 noel 4329 noelOLD 4330 vn0 4337 eq0 4342 ab0w 4372 ab0OLD 4374 ab0orv 4377 eq0rdv 4403 csbab 4436 disj 4446 rzal 4507 ralf0 4512 exss 5462 iotaeq 6505 abrexex2g 7946 opabex3d 7947 opabex3rd 7948 opabex3 7949 xpab 34633 eliminable1 35676 eliminable-velab 35682 bj-ab0 35726 bj-elabd2ALT 35743 bj-gabima 35758 bj-snsetex 35782 wl-clabv 36395 wl-clabtv 36397 wl-clabt 36398 elabgw 40963 ss2ab1 40984 scottabf 42932 |
Copyright terms: Public domain | W3C validator |