Theorem cbvesumv

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

	Ref	Expression
Hypothesis	cbvesum.1	|- ( j = k -> B = C )
Assertion	cbvesumv	|- sum* j e. A B = sum* k e. A C

Proof

Step	Hyp	Ref	Expression
1		cbvesum.1	|- ( j = k -> B = C )
2	1	cbvmptv	|- ( j e. A |-> B ) = ( k e. A |-> C )
3	2	oveq2i	|- ( ( RR*s |`s ( 0 [,] +oo ) ) tsums ( j e. A |-> B ) ) = ( ( RR*s |`s ( 0 [,] +oo ) ) tsums ( k e. A |-> C ) )
4	3	unieqi	|- U. ( ( RR*s |`s ( 0 [,] +oo ) ) tsums ( j e. A |-> B ) ) = U. ( ( RR*s |`s ( 0 [,] +oo ) ) tsums ( k e. A |-> C ) )
5		df-esum	|- sum* j e. A B = U. ( ( RR*s |`s ( 0 [,] +oo ) ) tsums ( j e. A |-> B ) )
6		df-esum	|- sum* k e. A C = U. ( ( RR*s |`s ( 0 [,] +oo ) ) tsums ( k e. A |-> C ) )
7	4 5 6	3eqtr4i	|- sum* j e. A B = sum* k e. A C