Theorem cbvsumi

Description: Change bound variable in a sum. (Contributed by NM, 11-Dec-2005)

	Ref	Expression
Hypotheses	cbvsumi.1	$$⊢\underset{\_}{Ⅎ}kB$$
	cbvsumi.2	$$⊢\underset{\_}{Ⅎ}jC$$
	cbvsumi.3	$$⊢j=k\to B=C$$
Assertion	cbvsumi	$$⊢\sum _{j\in A}B=\sum _{k\in A}C$$

Proof

Step	Hyp	Ref	Expression
1		cbvsumi.1	$$⊢\underset{\_}{Ⅎ}kB$$
2		cbvsumi.2	$$⊢\underset{\_}{Ⅎ}jC$$
3		cbvsumi.3	$$⊢j=k\to B=C$$
4		nfcv	$$⊢\underset{\_}{Ⅎ}kA$$
5		nfcv	$$⊢\underset{\_}{Ⅎ}jA$$
6	3 4 5 1 2	cbvsum	$$⊢\sum _{j\in A}B=\sum _{k\in A}C$$