Theorem cbvesumv

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

	Ref	Expression
Hypothesis	cbvesum.1	⊢ ( 𝑗 = 𝑘 → 𝐵 = 𝐶 )
Assertion	cbvesumv	⊢ Σ* 𝑗 ∈ 𝐴 𝐵 = Σ* 𝑘 ∈ 𝐴 𝐶

Proof

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