Theorem sumeq12i

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

	Ref	Expression
Hypotheses	sumeq12i.1	$$⊢A=B$$
	sumeq12i.2	$$⊢k\in A\to C=D$$
Assertion	sumeq12i	$$⊢\sum _{k\in A}C=\sum _{k\in B}D$$

Proof

Step	Hyp	Ref	Expression
1		sumeq12i.1	$$⊢A=B$$
2		sumeq12i.2	$$⊢k\in A\to C=D$$
3	2	sumeq2i	$$⊢\sum _{k\in A}C=\sum _{k\in A}D$$
4	1	sumeq1i	$$⊢\sum _{k\in A}D=\sum _{k\in B}D$$
5	3 4	eqtri	$$⊢\sum _{k\in A}C=\sum _{k\in B}D$$