Theorem cbvsumv

Description: Change bound variable in a sum. (Contributed by NM, 11-Dec-2005) (Revised by Mario Carneiro, 13-Jul-2013)

	Ref	Expression
Hypothesis	cbvsum.1	$$⊢j=k\to B=C$$
Assertion	cbvsumv	$$⊢\sum _{j\in A}B=\sum _{k\in A}C$$

Proof

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