| 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 3798). This is somewhat arbitrary: we could have, instead, chosen the conclusion of sbc6 3819 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 3790 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 3790, which holds for both our definition and Quine's, and from which we can derive a weaker version of df-sbc 3789 in the form of sbc8g 3796. 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 3789 and assert that [𝐴 / 𝑥]𝜑 is always false when 𝐴 is a proper class. Theorem sbc2or 3797 shows the apparently "strongest" statement we can make regarding behavior at proper classes if we start from dfsbcq 3790. The related definition df-csb 3900 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 3788 | . 2 wff [𝐴 / 𝑥]𝜑 |
| 5 | 1, 2 | cab 2714 | . . 3 class {𝑥 ∣ 𝜑} |
| 6 | 3, 5 | wcel 2108 | . 2 wff 𝐴 ∈ {𝑥 ∣ 𝜑} |
| 7 | 4, 6 | wb 206 | 1 wff ([𝐴 / 𝑥]𝜑 ↔ 𝐴 ∈ {𝑥 ∣ 𝜑}) |
| Colors of variables: wff setvar class |
| This definition is referenced by: dfsbcq 3790 dfsbcq2 3791 sbceqbid 3795 sbcex 3798 nfsbc1d 3806 nfsbcdw 3809 nfsbcd 3812 sbc5 3816 sbc6g 3818 cbvsbcw 3821 cbvsbcvw 3822 cbvsbc 3823 sbcieg 3828 sbcied 3832 sbcbid 3844 sbcbi2 3848 sbcimdv 3859 sbcg 3863 intab 4978 brab1 5191 iotacl 6547 riotasbc 7406 scottexs 9927 scott0s 9928 hta 9937 issubc 17880 dmdprd 20018 sbceqbidf 32506 bnj1454 34856 bnj110 34872 setinds 35779 sbceqbii 36192 cbvsbcvw2 36231 cbvsbcdavw 36258 cbvsbcdavw2 36259 bj-csbsnlem 36904 rdgssun 37379 frege54cor1c 43928 frege55lem1c 43929 frege55c 43931 |
| Copyright terms: Public domain | W3C validator |