Metamath Proof Explorer

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 nfcv 
 |-  F/_ k A
3 nfcv 
 |-  F/_ j A
4 nfcv 
 |-  F/_ k B
5 nfcv 
 |-  F/_ j C
6 1 2 3 4 5 cbvesum 
 |-  sum* j e. A B = sum* k e. A C