![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > dfsbcq | Structured version Visualization version GIF version |
Description: Proper substitution of a
class for a set in a wff given equal classes.
This is the essence of the sixth axiom of Frege, specifically Proposition
52 of [Frege1879] p. 50.
This theorem, which is similar to Theorem 6.7 of [Quine] p. 42 and holds under both our definition and Quine's, provides us with a weak definition of the proper substitution of a class for a set. Since our df-sbc 3777 does not result in the same behavior as Quine's for proper classes, if we wished to avoid conflict with Quine's definition we could start with this theorem and dfsbcq2 3779 instead of df-sbc 3777. (dfsbcq2 3779 is needed because unlike Quine we do not overload the df-sb 2061 syntax.) As a consequence of these theorems, we can derive sbc8g 3784, which is a weaker version of df-sbc 3777 that leaves substitution undefined when 𝐴 is a proper class. However, it is often a nuisance to have to prove the sethood hypothesis of sbc8g 3784, so we will allow direct use of df-sbc 3777 after Theorem sbc2or 3785 below. Proper substitution with a proper class is rarely needed, and when it is, we can simply use the expansion of Quine's definition. (Contributed by NM, 14-Apr-1995.) |
Ref | Expression |
---|---|
dfsbcq | ⊢ (𝐴 = 𝐵 → ([𝐴 / 𝑥]𝜑 ↔ [𝐵 / 𝑥]𝜑)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eleq1 2814 | . 2 ⊢ (𝐴 = 𝐵 → (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ 𝐵 ∈ {𝑥 ∣ 𝜑})) | |
2 | df-sbc 3777 | . 2 ⊢ ([𝐴 / 𝑥]𝜑 ↔ 𝐴 ∈ {𝑥 ∣ 𝜑}) | |
3 | df-sbc 3777 | . 2 ⊢ ([𝐵 / 𝑥]𝜑 ↔ 𝐵 ∈ {𝑥 ∣ 𝜑}) | |
4 | 1, 2, 3 | 3bitr4g 313 | 1 ⊢ (𝐴 = 𝐵 → ([𝐴 / 𝑥]𝜑 ↔ [𝐵 / 𝑥]𝜑)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 = wceq 1534 ∈ wcel 2099 {cab 2703 [wsbc 3776 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-ext 2697 |
This theorem depends on definitions: df-bi 206 df-an 395 df-ex 1775 df-cleq 2718 df-clel 2803 df-sbc 3777 |
This theorem is referenced by: sbceq1d 3781 sbc8g 3784 spsbc 3789 sbccow 3799 sbcco 3802 sbcco2 3803 sbcie2g 3819 elrabsf 3825 eqsbc1 3826 csbeq1 3895 cbvralcsf 3937 sbcnestgfw 4423 sbcco3gw 4427 sbcnestgf 4428 sbcco3g 4432 csbie2df 4445 reusngf 4681 reuprg0 4711 sbcop 5495 reuop 6304 ralrnmptw 7108 ralrnmpt 7110 tfindes 7873 findcard2 9202 findcard2OLD 9318 ac6sfi 9321 indexfi 9404 nn1suc 12286 uzind4s2 12945 wrdind 14730 wrd2ind 14731 prmind2 16686 mndind 18818 elmptrab 23822 isfildlem 23852 ifeqeqx 32463 wrdt2ind 32817 bnj609 34762 bnj601 34765 sdclem2 37443 fdc1 37447 sbccom2 37826 sbccom2f 37827 sbccom2fi 37828 elimhyps 38659 dedths 38660 elimhyps2 38662 dedths2 38663 lshpkrlem3 38810 rexrabdioph 42451 rexfrabdioph 42452 2rexfrabdioph 42453 3rexfrabdioph 42454 4rexfrabdioph 42455 6rexfrabdioph 42456 7rexfrabdioph 42457 2nn0ind 42603 zindbi 42604 axfrege52c 43554 frege58c 43588 frege92 43622 2sbc6g 44089 2sbc5g 44090 pm14.122b 44097 pm14.24 44106 iotavalsb 44107 sbiota1 44108 fvsb 44126 or2expropbilem1 46647 ich2exprop 47043 reupr 47094 |
Copyright terms: Public domain | W3C validator |