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 j A B = k A C

Proof

Step Hyp Ref Expression
1 cbvsum.1 j = k B = C
2 nfcv _ k A
3 nfcv _ j A
4 nfcv _ k B
5 nfcv _ j C
6 1 2 3 4 5 cbvsum j A B = k A C