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	⊢ ( 𝑗 = 𝑘 → 𝐵 = 𝐶 )
Assertion	cbvsumv	⊢ Σ 𝑗 ∈ 𝐴 𝐵 = Σ 𝑘 ∈ 𝐴 𝐶

Proof

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