# Metamath Proof Explorer

## Theorem cbvsum

Description: Change bound variable in a sum. (Contributed by NM, 11-Dec-2005) (Revised by Mario Carneiro, 13-Jun-2019)

Ref Expression
Hypotheses cbvsum.1 ${⊢}{j}={k}\to {B}={C}$
cbvsum.2 ${⊢}\underset{_}{Ⅎ}{k}\phantom{\rule{.4em}{0ex}}{A}$
cbvsum.3 ${⊢}\underset{_}{Ⅎ}{j}\phantom{\rule{.4em}{0ex}}{A}$
cbvsum.4 ${⊢}\underset{_}{Ⅎ}{k}\phantom{\rule{.4em}{0ex}}{B}$
cbvsum.5 ${⊢}\underset{_}{Ⅎ}{j}\phantom{\rule{.4em}{0ex}}{C}$
Assertion cbvsum ${⊢}\sum _{{j}\in {A}}{B}=\sum _{{k}\in {A}}{C}$

### Proof

Step Hyp Ref Expression
1 cbvsum.1 ${⊢}{j}={k}\to {B}={C}$
2 cbvsum.2 ${⊢}\underset{_}{Ⅎ}{k}\phantom{\rule{.4em}{0ex}}{A}$
3 cbvsum.3 ${⊢}\underset{_}{Ⅎ}{j}\phantom{\rule{.4em}{0ex}}{A}$
4 cbvsum.4 ${⊢}\underset{_}{Ⅎ}{k}\phantom{\rule{.4em}{0ex}}{B}$
5 cbvsum.5 ${⊢}\underset{_}{Ⅎ}{j}\phantom{\rule{.4em}{0ex}}{C}$
6 4 5 1 cbvcsbw
7 6 a1i
8 7 ifeq1d
9 8 mpteq2dv
10 9 seqeq3d
11 10 mptru
12 11 breq1i
13 12 anbi2i
14 13 rexbii
15 4 5 1 cbvcsbw
16 15 a1i
17 16 mpteq2dv
18 17 seqeq3d
19 18 mptru
20 19 fveq1i
21 20 eqeq2i
22 21 anbi2i
23 22 exbii
24 23 rexbii
25 14 24 orbi12i
26 25 iotabii
27 df-sum
28 df-sum
29 26 27 28 3eqtr4i ${⊢}\sum _{{j}\in {A}}{B}=\sum _{{k}\in {A}}{C}$