![]() |
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 3740 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 3742 instead of df-sbc 3740. (dfsbcq2 3742 is needed because unlike Quine we do not overload the df-sb 2068 syntax.) As a consequence of these theorems, we can derive sbc8g 3747, which is a weaker version of df-sbc 3740 that leaves substitution undefined when 𝐴 is a proper class. However, it is often a nuisance to have to prove the sethood hypothesis of sbc8g 3747, so we will allow direct use of df-sbc 3740 after Theorem sbc2or 3748 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 2825 | . 2 ⊢ (𝐴 = 𝐵 → (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ 𝐵 ∈ {𝑥 ∣ 𝜑})) | |
2 | df-sbc 3740 | . 2 ⊢ ([𝐴 / 𝑥]𝜑 ↔ 𝐴 ∈ {𝑥 ∣ 𝜑}) | |
3 | df-sbc 3740 | . 2 ⊢ ([𝐵 / 𝑥]𝜑 ↔ 𝐵 ∈ {𝑥 ∣ 𝜑}) | |
4 | 1, 2, 3 | 3bitr4g 313 | 1 ⊢ (𝐴 = 𝐵 → ([𝐴 / 𝑥]𝜑 ↔ [𝐵 / 𝑥]𝜑)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 = wceq 1541 ∈ wcel 2106 {cab 2713 [wsbc 3739 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2707 |
This theorem depends on definitions: df-bi 206 df-an 397 df-ex 1782 df-cleq 2728 df-clel 2814 df-sbc 3740 |
This theorem is referenced by: sbceq1d 3744 sbc8g 3747 spsbc 3752 sbccow 3762 sbcco 3765 sbcco2 3766 sbcie2g 3781 elrabsf 3787 eqsbc1 3788 csbeq1 3858 cbvralcsf 3900 sbcnestgfw 4378 sbcco3gw 4382 sbcnestgf 4383 sbcco3g 4387 csbie2df 4400 reusngf 4633 reuprg0 4663 sbcop 5446 reuop 6245 ralrnmptw 7043 ralrnmpt 7045 tfindes 7798 findcard2 9107 findcard2OLD 9227 ac6sfi 9230 indexfi 9303 nn1suc 12174 uzind4s2 12833 wrdind 14609 wrd2ind 14610 prmind2 16560 mndind 18637 elmptrab 23176 isfildlem 23206 ifeqeqx 31462 wrdt2ind 31802 bnj609 33520 bnj601 33523 sdclem2 36192 fdc1 36196 sbccom2 36575 sbccom2f 36576 sbccom2fi 36577 elimhyps 37414 dedths 37415 elimhyps2 37417 dedths2 37418 lshpkrlem3 37565 rexrabdioph 41095 rexfrabdioph 41096 2rexfrabdioph 41097 3rexfrabdioph 41098 4rexfrabdioph 41099 6rexfrabdioph 41100 7rexfrabdioph 41101 2nn0ind 41247 zindbi 41248 axfrege52c 42141 frege58c 42175 frege92 42209 2sbc6g 42677 2sbc5g 42678 pm14.122b 42685 pm14.24 42694 iotavalsb 42695 sbiota1 42696 fvsb 42714 or2expropbilem1 45238 ich2exprop 45635 reupr 45686 |
Copyright terms: Public domain | W3C validator |