This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem sumeq1i

Description: Equality inference for sum. (Contributed by NM, 2-Jan-2006)

Ref Expression
Hypothesis sumeq1i.1 
|- A = B
Assertion sumeq1i 
|- sum_ k e. A C = sum_ k e. B C

Proof

Step Hyp Ref Expression
1 sumeq1i.1 
 |-  A = B
2 sumeq1 
 |-  ( A = B -> sum_ k e. A C = sum_ k e. B C )
3 1 2 ax-mp 
 |-  sum_ k e. A C = sum_ k e. B C