![]() |
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 3741 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 3743 instead of df-sbc 3741. (dfsbcq2 3743 is needed because unlike Quine we do not overload the df-sb 2069 syntax.) As a consequence of these theorems, we can derive sbc8g 3748, which is a weaker version of df-sbc 3741 that leaves substitution undefined when 𝐴 is a proper class. However, it is often a nuisance to have to prove the sethood hypothesis of sbc8g 3748, so we will allow direct use of df-sbc 3741 after Theorem sbc2or 3749 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 2822 | . 2 ⊢ (𝐴 = 𝐵 → (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ 𝐵 ∈ {𝑥 ∣ 𝜑})) | |
2 | df-sbc 3741 | . 2 ⊢ ([𝐴 / 𝑥]𝜑 ↔ 𝐴 ∈ {𝑥 ∣ 𝜑}) | |
3 | df-sbc 3741 | . 2 ⊢ ([𝐵 / 𝑥]𝜑 ↔ 𝐵 ∈ {𝑥 ∣ 𝜑}) | |
4 | 1, 2, 3 | 3bitr4g 314 | 1 ⊢ (𝐴 = 𝐵 → ([𝐴 / 𝑥]𝜑 ↔ [𝐵 / 𝑥]𝜑)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 = wceq 1542 ∈ wcel 2107 {cab 2710 [wsbc 3740 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-ext 2704 |
This theorem depends on definitions: df-bi 206 df-an 398 df-ex 1783 df-cleq 2725 df-clel 2811 df-sbc 3741 |
This theorem is referenced by: sbceq1d 3745 sbc8g 3748 spsbc 3753 sbccow 3763 sbcco 3766 sbcco2 3767 sbcie2g 3782 elrabsf 3788 eqsbc1 3789 csbeq1 3859 cbvralcsf 3901 sbcnestgfw 4379 sbcco3gw 4383 sbcnestgf 4384 sbcco3g 4388 csbie2df 4401 reusngf 4634 reuprg0 4664 sbcop 5447 reuop 6246 ralrnmptw 7045 ralrnmpt 7047 tfindes 7800 findcard2 9111 findcard2OLD 9231 ac6sfi 9234 indexfi 9307 nn1suc 12180 uzind4s2 12839 wrdind 14616 wrd2ind 14617 prmind2 16566 mndind 18643 elmptrab 23194 isfildlem 23224 ifeqeqx 31507 wrdt2ind 31856 bnj609 33586 bnj601 33589 sdclem2 36247 fdc1 36251 sbccom2 36630 sbccom2f 36631 sbccom2fi 36632 elimhyps 37469 dedths 37470 elimhyps2 37472 dedths2 37473 lshpkrlem3 37620 rexrabdioph 41160 rexfrabdioph 41161 2rexfrabdioph 41162 3rexfrabdioph 41163 4rexfrabdioph 41164 6rexfrabdioph 41165 7rexfrabdioph 41166 2nn0ind 41312 zindbi 41313 axfrege52c 42247 frege58c 42281 frege92 42315 2sbc6g 42783 2sbc5g 42784 pm14.122b 42791 pm14.24 42800 iotavalsb 42801 sbiota1 42802 fvsb 42820 or2expropbilem1 45352 ich2exprop 45749 reupr 45800 |
Copyright terms: Public domain | W3C validator |