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