![]() |
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 2825 | . . . 4 ⊢ (𝜑 → (𝑦 ∈ 𝐵 ↔ 𝑦 ∈ 𝐶)) |
3 | 2 | sbcbidv 3851 | . . 3 ⊢ (𝜑 → ([𝐴 / 𝑥]𝑦 ∈ 𝐵 ↔ [𝐴 / 𝑥]𝑦 ∈ 𝐶)) |
4 | 3 | abbidv 2806 | . 2 ⊢ (𝜑 → {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵} = {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐶}) |
5 | df-csb 3909 | . 2 ⊢ ⦋𝐴 / 𝑥⦌𝐵 = {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵} | |
6 | df-csb 3909 | . 2 ⊢ ⦋𝐴 / 𝑥⦌𝐶 = {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐶} | |
7 | 4, 5, 6 | 3eqtr4g 2800 | 1 ⊢ (𝜑 → ⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1537 ∈ wcel 2106 {cab 2712 [wsbc 3791 ⦋csb 3908 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1908 ax-6 1965 ax-7 2005 ax-8 2108 ax-9 2116 ax-ext 2706 |
This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1777 df-sb 2063 df-clab 2713 df-cleq 2727 df-clel 2814 df-sbc 3792 df-csb 3909 |
This theorem is referenced by: csbeq2i 3916 csbeq12dv 3917 mpomptsx 8088 dmmpossx 8090 fmpox 8091 el2mpocsbcl 8109 offval22 8112 ovmptss 8117 fmpoco 8119 mposn 8127 mpocurryd 8293 fvmpocurryd 8295 cantnffval 9701 sumeq2sdv 15736 fsumcom2 15807 prodeq2sdv 15956 fprodcom2 16017 bpolylem 16081 bpolyval 16082 ruclem1 16264 natfval 18001 fucval 18014 evlfval 18274 rnghmval 20457 mpfrcl 22127 selvffval 22155 selvfval 22156 selvval 22157 pmatcollpw3lem 22805 fsumcn 24908 fsum2cn 24909 itgeq1f 25821 itgeq1 25823 dvmptfsum 26028 mulsval 28150 precsexlemcbv 28245 ttgvalOLD 28899 msrfval 35522 poimirlem5 37612 poimirlem6 37613 poimirlem7 37614 poimirlem8 37615 poimirlem10 37617 poimirlem11 37618 poimirlem12 37619 poimirlem15 37622 poimirlem18 37625 poimirlem21 37628 poimirlem22 37629 poimirlem24 37631 poimirlem26 37633 poimirlem27 37634 cdleme31sde 40368 cdlemeg47rv2 40493 dmmpossx2 48182 |
Copyright terms: Public domain | W3C validator |