Theorem cbvsumi

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

	Ref	Expression
Hypotheses	cbvsumi.1	⊢ Ⅎ 𝑘 𝐵
	cbvsumi.2	⊢ Ⅎ 𝑗 𝐶
	cbvsumi.3	⊢ ( 𝑗 = 𝑘 → 𝐵 = 𝐶 )
Assertion	cbvsumi	⊢ Σ 𝑗 ∈ 𝐴 𝐵 = Σ 𝑘 ∈ 𝐴 𝐶

Proof

Step	Hyp	Ref	Expression
1		cbvsumi.1	⊢ Ⅎ 𝑘 𝐵
2		cbvsumi.2	⊢ Ⅎ 𝑗 𝐶
3		cbvsumi.3	⊢ ( 𝑗 = 𝑘 → 𝐵 = 𝐶 )
4		nfcv	⊢ Ⅎ 𝑘 𝐴
5		nfcv	⊢ Ⅎ 𝑗 𝐴
6	3 4 5 1 2	cbvsum	⊢ Σ 𝑗 ∈ 𝐴 𝐵 = Σ 𝑘 ∈ 𝐴 𝐶