Metamath Proof Explorer


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
|- ( j = k -> B = C )
Assertion cbvsumv
|- sum_ j e. A B = sum_ k e. A C

Proof

Step Hyp Ref Expression
1 cbvsum.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 cbvsum
 |-  sum_ j e. A B = sum_ k e. A C