Metamath Proof Explorer


Theorem cbvsumi

Description: Change bound variable in a sum. (Contributed by NM, 11-Dec-2005)

Ref Expression
Hypotheses cbvsumi.1 _ k B
cbvsumi.2 _ j C
cbvsumi.3 j = k B = C
Assertion cbvsumi j A B = k A C

Proof

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