|   | Metamath Proof Explorer | < Previous  
      Next > Nearby theorems | |
| Mirrors > Home > MPE Home > Th. List > csbeq2dv | Structured version Visualization version GIF version | ||
| Description: Formula-building deduction for class substitution. (Contributed by NM, 10-Nov-2005.) (Revised by Mario Carneiro, 1-Sep-2015.) | 
| Ref | Expression | 
|---|---|
| csbeq2dv.1 | ⊢ (𝜑 → 𝐵 = 𝐶) | 
| Ref | Expression | 
|---|---|
| csbeq2dv | ⊢ (𝜑 → ⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐶) | 
| Step | Hyp | Ref | Expression | 
|---|---|---|---|
| 1 | csbeq2dv.1 | . . . . 5 ⊢ (𝜑 → 𝐵 = 𝐶) | |
| 2 | 1 | eleq2d 2827 | . . . 4 ⊢ (𝜑 → (𝑦 ∈ 𝐵 ↔ 𝑦 ∈ 𝐶)) | 
| 3 | 2 | sbcbidv 3845 | . . 3 ⊢ (𝜑 → ([𝐴 / 𝑥]𝑦 ∈ 𝐵 ↔ [𝐴 / 𝑥]𝑦 ∈ 𝐶)) | 
| 4 | 3 | abbidv 2808 | . 2 ⊢ (𝜑 → {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵} = {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐶}) | 
| 5 | df-csb 3900 | . 2 ⊢ ⦋𝐴 / 𝑥⦌𝐵 = {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵} | |
| 6 | df-csb 3900 | . 2 ⊢ ⦋𝐴 / 𝑥⦌𝐶 = {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐶} | |
| 7 | 4, 5, 6 | 3eqtr4g 2802 | 1 ⊢ (𝜑 → ⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐶) | 
| Colors of variables: wff setvar class | 
| Syntax hints: → wi 4 = wceq 1540 ∈ wcel 2108 {cab 2714 [wsbc 3788 ⦋csb 3899 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 | 
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-sbc 3789 df-csb 3900 | 
| This theorem is referenced by: csbeq2i 3907 csbeq12dv 3908 mpomptsx 8089 dmmpossx 8091 fmpox 8092 el2mpocsbcl 8110 offval22 8113 ovmptss 8118 fmpoco 8120 mposn 8128 mpocurryd 8294 fvmpocurryd 8296 cantnffval 9703 sumeq2sdv 15739 fsumcom2 15810 prodeq2sdv 15959 fprodcom2 16020 bpolylem 16084 bpolyval 16085 ruclem1 16267 natfval 17994 fucval 18006 evlfval 18262 rnghmval 20440 mpfrcl 22109 selvffval 22137 selvfval 22138 selvval 22139 pmatcollpw3lem 22789 fsumcn 24894 fsum2cn 24895 itgeq1f 25806 itgeq1 25808 dvmptfsum 26013 mulsval 28135 precsexlemcbv 28230 ttgvalOLD 28884 msrfval 35542 poimirlem5 37632 poimirlem6 37633 poimirlem7 37634 poimirlem8 37635 poimirlem10 37637 poimirlem11 37638 poimirlem12 37639 poimirlem15 37642 poimirlem18 37645 poimirlem21 37648 poimirlem22 37649 poimirlem24 37651 poimirlem26 37653 poimirlem27 37654 cdleme31sde 40387 cdlemeg47rv2 40512 dmmpossx2 48253 dfswapf2 48967 fucofvalg 49013 | 
| Copyright terms: Public domain | W3C validator |