| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > df-sbc | Structured version Visualization version GIF version | ||
| Description: Define the proper
substitution of a class for a set.
When 𝐴 is a proper class, our definition evaluates to false (see sbcex 3751). This is somewhat arbitrary: we could have, instead, chosen the conclusion of sbc6 3772 for our definition, whose right-hand side always evaluates to true for proper classes. Our definition also does not produce the same results as discussed in the proof of Theorem 6.6 of [Quine] p. 42 (although Theorem 6.6 itself does hold, as shown by dfsbcq 3743 below). For example, if 𝐴 is a proper class, Quine's substitution of 𝐴 for 𝑦 in 0 ∈ 𝑦 evaluates to 0 ∈ 𝐴 rather than our falsehood. (This can be seen by substituting 𝐴, 𝑦, and 0 for alpha, beta, and gamma in Subcase 1 of Quine's discussion on p. 42.) Unfortunately, Quine's definition requires a recursive syntactic breakdown of 𝜑, and it does not seem possible to express it with a single closed formula. If we did not want to commit to any specific proper class behavior, we could use this definition only to prove Theorem dfsbcq 3743, which holds for both our definition and Quine's, and from which we can derive a weaker version of df-sbc 3742 in the form of sbc8g 3749. However, the behavior of Quine's definition at proper classes is similarly arbitrary, and for practical reasons (to avoid having to prove sethood of 𝐴 in every use of this definition) we allow direct reference to df-sbc 3742 and assert that [𝐴 / 𝑥]𝜑 is always false when 𝐴 is a proper class. Theorem sbc2or 3750 shows the apparently "strongest" statement we can make regarding behavior at proper classes if we start from dfsbcq 3743. The related definition df-csb 3851 defines proper substitution into a class variable (as opposed to a wff variable). (Contributed by NM, 14-Apr-1995.) (Revised by NM, 25-Dec-2016.) |
| Ref | Expression |
|---|---|
| df-sbc | ⊢ ([𝐴 / 𝑥]𝜑 ↔ 𝐴 ∈ {𝑥 ∣ 𝜑}) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | wph | . . 3 wff 𝜑 | |
| 2 | vx | . . 3 setvar 𝑥 | |
| 3 | cA | . . 3 class 𝐴 | |
| 4 | 1, 2, 3 | wsbc 3741 | . 2 wff [𝐴 / 𝑥]𝜑 |
| 5 | 1, 2 | cab 2715 | . . 3 class {𝑥 ∣ 𝜑} |
| 6 | 3, 5 | wcel 2114 | . 2 wff 𝐴 ∈ {𝑥 ∣ 𝜑} |
| 7 | 4, 6 | wb 206 | 1 wff ([𝐴 / 𝑥]𝜑 ↔ 𝐴 ∈ {𝑥 ∣ 𝜑}) |
| Colors of variables: wff setvar class |
| This definition is referenced by: dfsbcq 3743 dfsbcq2 3744 sbceqbid 3748 sbcex 3751 nfsbc1d 3759 nfsbcdw 3762 nfsbcd 3765 sbc5 3769 sbc6g 3771 cbvsbcw 3774 cbvsbcvw 3775 cbvsbc 3776 sbcieg 3781 sbcied 3785 sbcbid 3796 sbcbi2 3800 sbcimdv 3810 sbcg 3814 intab 4934 brab1 5147 iotacl 6479 riotasbc 7335 setinds 9662 scottexs 9803 scott0s 9804 hta 9813 issubc 17763 dmdprd 19933 sbceqbidf 32564 bnj1454 35000 bnj110 35016 sbceqbii 36387 cbvsbcvw2 36426 cbvsbcdavw 36453 cbvsbcdavw2 36454 bj-csbsnlem 37106 rdgssun 37585 frege54cor1c 44223 frege55lem1c 44224 frege55c 44226 |
| Copyright terms: Public domain | W3C validator |