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