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