Theorem cbvsumi

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

	Ref	Expression
Hypotheses	cbvsumi.1	|- F/_ k B
	cbvsumi.2	|- F/_ j C
	cbvsumi.3	|- ( j = k -> B = C )
Assertion	cbvsumi	|- sum_ j e. A B = sum_ k e. A C

Proof

Step	Hyp	Ref	Expression
1		cbvsumi.1	|- F/_ k B
2		cbvsumi.2	|- F/_ j C
3		cbvsumi.3	|- ( j = k -> B = C )
4		nfcv	|- F/_ k A
5		nfcv	|- F/_ j A
6	3 4 5 1 2	cbvsum	|- sum_ j e. A B = sum_ k e. A C