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 | |
|
cbvsum.2 | |
||
cbvsum.3 | |
||
cbvsum.4 | |
||
cbvsum.5 | |
||
Assertion | cbvsum | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cbvsum.1 | |
|
2 | cbvsum.2 | |
|
3 | cbvsum.3 | |
|
4 | cbvsum.4 | |
|
5 | cbvsum.5 | |
|
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 | |