Theorem cbvesum

Description: Change bound variable in an extended sum. (Contributed by Thierry Arnoux, 19-Jun-2017)

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

Proof

Step	Hyp	Ref	Expression
1		cbvesum.1	⊢ ( 𝑗 = 𝑘 → 𝐵 = 𝐶 )
2		cbvesum.2	⊢ Ⅎ 𝑘 𝐴
3		cbvesum.3	⊢ Ⅎ 𝑗 𝐴
4		cbvesum.4	⊢ Ⅎ 𝑘 𝐵
5		cbvesum.5	⊢ Ⅎ 𝑗 𝐶
6	3 2 4 5 1	cbvmptf	⊢ ( 𝑗 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑘 ∈ 𝐴 ↦ 𝐶 )
7	6	oveq2i	⊢ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) tsums ( 𝑗 ∈ 𝐴 ↦ 𝐵 ) ) = ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) tsums ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) )
8	7	unieqi	⊢ ∪ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) tsums ( 𝑗 ∈ 𝐴 ↦ 𝐵 ) ) = ∪ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) tsums ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) )
9		df-esum	⊢ Σ* 𝑗 ∈ 𝐴 𝐵 = ∪ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) tsums ( 𝑗 ∈ 𝐴 ↦ 𝐵 ) )
10		df-esum	⊢ Σ* 𝑘 ∈ 𝐴 𝐶 = ∪ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) tsums ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) )
11	8 9 10	3eqtr4i	⊢ Σ* 𝑗 ∈ 𝐴 𝐵 = Σ* 𝑘 ∈ 𝐴 𝐶