|   | 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 3788 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 3790 instead of df-sbc 3788. (dfsbcq2 3790 is needed because unlike Quine we do not overload the df-sb 2064 syntax.) As a consequence of these theorems, we can derive sbc8g 3795, which is a weaker version of df-sbc 3788 that leaves substitution undefined when 𝐴 is a proper class. However, it is often a nuisance to have to prove the sethood hypothesis of sbc8g 3795, so we will allow direct use of df-sbc 3788 after Theorem sbc2or 3796 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 2828 | . 2 ⊢ (𝐴 = 𝐵 → (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ 𝐵 ∈ {𝑥 ∣ 𝜑})) | |
| 2 | df-sbc 3788 | . 2 ⊢ ([𝐴 / 𝑥]𝜑 ↔ 𝐴 ∈ {𝑥 ∣ 𝜑}) | |
| 3 | df-sbc 3788 | . 2 ⊢ ([𝐵 / 𝑥]𝜑 ↔ 𝐵 ∈ {𝑥 ∣ 𝜑}) | |
| 4 | 1, 2, 3 | 3bitr4g 314 | 1 ⊢ (𝐴 = 𝐵 → ([𝐴 / 𝑥]𝜑 ↔ [𝐵 / 𝑥]𝜑)) | 
| Colors of variables: wff setvar class | 
| Syntax hints: → wi 4 ↔ wb 206 = wceq 1539 ∈ wcel 2107 {cab 2713 [wsbc 3787 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 ax-5 1909 ax-6 1966 ax-7 2006 ax-8 2109 ax-9 2117 ax-ext 2707 | 
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1779 df-cleq 2728 df-clel 2815 df-sbc 3788 | 
| This theorem is referenced by: sbceq1d 3792 sbc8g 3795 spsbc 3800 sbccow 3810 sbcco 3813 sbcco2 3814 sbcie2g 3828 elrabsf 3833 eqsbc1 3834 csbeq1 3901 cbvralcsf 3940 sbcnestgfw 4420 sbcco3gw 4424 sbcnestgf 4425 sbcco3g 4429 csbie2df 4442 reusngf 4673 reuprg0 4701 sbcop 5493 reuop 6312 ralrnmptw 7113 ralrnmpt 7115 tfindes 7885 findcard2 9205 ac6sfi 9321 indexfi 9401 nn1suc 12289 uzind4s2 12952 wrdind 14761 wrd2ind 14762 prmind2 16723 mndind 18842 elmptrab 23836 isfildlem 23866 ifeqeqx 32556 wrdt2ind 32939 bnj609 34932 bnj601 34935 weiunlem2 36465 sdclem2 37750 fdc1 37754 sbccom2 38133 sbccom2f 38134 sbccom2fi 38135 elimhyps 38963 dedths 38964 elimhyps2 38966 dedths2 38967 lshpkrlem3 39114 rexrabdioph 42810 rexfrabdioph 42811 2rexfrabdioph 42812 3rexfrabdioph 42813 4rexfrabdioph 42814 6rexfrabdioph 42815 7rexfrabdioph 42816 2nn0ind 42962 zindbi 42963 axfrege52c 43905 frege58c 43939 frege92 43973 2sbc6g 44439 2sbc5g 44440 pm14.122b 44447 pm14.24 44456 iotavalsb 44457 sbiota1 44458 fvsb 44476 or2expropbilem1 47049 ich2exprop 47463 reupr 47514 | 
| Copyright terms: Public domain | W3C validator |