![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > sumeq1i | Structured version Visualization version GIF version |
Description: Equality inference for sum. (Contributed by NM, 2-Jan-2006.) |
Ref | Expression |
---|---|
sumeq1i.1 | ⊢ 𝐴 = 𝐵 |
Ref | Expression |
---|---|
sumeq1i | ⊢ Σ𝑘 ∈ 𝐴 𝐶 = Σ𝑘 ∈ 𝐵 𝐶 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sumeq1i.1 | . 2 ⊢ 𝐴 = 𝐵 | |
2 | sumeq1 14507 | . 2 ⊢ (𝐴 = 𝐵 → Σ𝑘 ∈ 𝐴 𝐶 = Σ𝑘 ∈ 𝐵 𝐶) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ Σ𝑘 ∈ 𝐴 𝐶 = Σ𝑘 ∈ 𝐵 𝐶 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1564 Σcsu 14504 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1818 ax-5 1920 ax-6 1986 ax-7 2022 ax-9 2080 ax-10 2100 ax-11 2115 ax-12 2128 ax-13 2323 ax-ext 2672 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-3an 1074 df-tru 1567 df-ex 1786 df-nf 1791 df-sb 1979 df-clab 2679 df-cleq 2685 df-clel 2688 df-nfc 2823 df-ral 2987 df-rex 2988 df-rab 2991 df-v 3274 df-dif 3651 df-un 3653 df-in 3655 df-ss 3662 df-nul 3992 df-if 4163 df-sn 4254 df-pr 4256 df-op 4260 df-uni 4513 df-br 4729 df-opab 4789 df-mpt 4806 df-xp 5192 df-cnv 5194 df-dm 5196 df-rn 5197 df-res 5198 df-ima 5199 df-pred 5761 df-iota 5932 df-f 5973 df-f1 5974 df-fo 5975 df-f1o 5976 df-fv 5977 df-ov 6736 df-oprab 6737 df-mpt2 6738 df-wrecs 7495 df-recs 7556 df-rdg 7594 df-seq 12885 df-sum 14505 |
This theorem is referenced by: sumeq12i 14518 fsump1i 14588 fsum2d 14590 fsumxp 14591 isumnn0nn 14662 arisum 14680 arisum2 14681 geo2sum 14692 bpoly0 14869 bpoly1 14870 bpoly2 14876 bpoly3 14877 bpoly4 14878 efsep 14928 ef4p 14931 rpnnen2lem12 15042 ovolicc2lem4 23377 itg10 23543 dveflem 23830 dvply1 24127 vieta1lem2 24154 aaliou3lem4 24189 dvtaylp 24212 pserdvlem2 24270 advlogexp 24489 log2ublem2 24762 log2ublem3 24763 log2ub 24764 ftalem5 24891 cht1 24979 1sgmprm 25012 lgsquadlem2 25194 axlowdimlem16 25925 finsumvtxdg2ssteplem4 26543 rusgrnumwwlks 26985 signsvf0 30855 signsvf1 30856 repr0 30887 k0004val0 38839 binomcxplemnotnn0 38942 fsumiunss 40195 dvnmul 40546 stoweidlem17 40622 dirkertrigeqlem1 40703 etransclem24 40863 etransclem35 40874 |
Copyright terms: Public domain | W3C validator |