Theorem sumeq2

Description: Equality theorem for sum. (Contributed by NM, 11-Dec-2005) (Revised by Mario Carneiro, 13-Jul-2013)

	Ref	Expression
Assertion	sumeq2	$$⊢\forall k\in AB=C\to \sum _{k\in A}B=\sum _{k\in A}C$$

Proof

Step	Hyp	Ref	Expression
1		fveq2	$$⊢B=C\to \mathrm{I}\left(B\right)=\mathrm{I}\left(C\right)$$
2	1	ralimi	$$⊢\forall k\in AB=C\to \forall k\in A\mathrm{I}\left(B\right)=\mathrm{I}\left(C\right)$$
3		sumeq2ii	$$⊢\forall k\in A\mathrm{I}\left(B\right)=\mathrm{I}\left(C\right)\to \sum _{k\in A}B=\sum _{k\in A}C$$
4	2 3	syl	$$⊢\forall k\in AB=C\to \sum _{k\in A}B=\sum _{k\in A}C$$