Description: Equality theorem for sum, when the class expressions B and C are equal everywhere. Proved using only Extensionality. (Contributed by Mario Carneiro, 24-Jun-2014) (Revised by Mario Carneiro, 13-Jun-2019)
Ref | Expression | ||
---|---|---|---|
Assertion | sumeq2w | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | csbeq2 | |
|
2 | 1 | ifeq1d | |
3 | 2 | mpteq2dv | |
4 | 3 | seqeq3d | |
5 | 4 | breq1d | |
6 | 5 | anbi2d | |
7 | 6 | rexbidv | |
8 | csbeq2 | |
|
9 | 8 | mpteq2dv | |
10 | 9 | seqeq3d | |
11 | 10 | fveq1d | |
12 | 11 | eqeq2d | |
13 | 12 | anbi2d | |
14 | 13 | exbidv | |
15 | 14 | rexbidv | |
16 | 7 15 | orbi12d | |
17 | 16 | iotabidv | |
18 | df-sum | |
|
19 | df-sum | |
|
20 | 17 18 19 | 3eqtr4g | |