Metamath Proof Explorer


Theorem sumeq12i

Description: Equality inference for sum. (Contributed by FL, 10-Dec-2006)

Ref Expression
Hypotheses sumeq12i.1
|- A = B
sumeq12i.2
|- ( k e. A -> C = D )
Assertion sumeq12i
|- sum_ k e. A C = sum_ k e. B D

Proof

Step Hyp Ref Expression
1 sumeq12i.1
 |-  A = B
2 sumeq12i.2
 |-  ( k e. A -> C = D )
3 2 sumeq2i
 |-  sum_ k e. A C = sum_ k e. A D
4 1 sumeq1i
 |-  sum_ k e. A D = sum_ k e. B D
5 3 4 eqtri
 |-  sum_ k e. A C = sum_ k e. B D