Description: Equality theorem for product, when the class expressions B and C are equal everywhere. Proved using only Extensionality. (Contributed by Scott Fenton, 4-Dec-2017)
Ref | Expression | ||
---|---|---|---|
Assertion | prodeq2w | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqid | |
|
2 | ifeq1 | |
|
3 | 2 | alimi | |
4 | alral | |
|
5 | 3 4 | syl | |
6 | mpteq12 | |
|
7 | 1 5 6 | sylancr | |
8 | 7 | seqeq3d | |
9 | 8 | breq1d | |
10 | 9 | anbi2d | |
11 | 10 | exbidv | |
12 | 11 | rexbidv | |
13 | 7 | seqeq3d | |
14 | 13 | breq1d | |
15 | 12 14 | 3anbi23d | |
16 | 15 | rexbidv | |
17 | csbeq2 | |
|
18 | 17 | mpteq2dv | |
19 | 18 | seqeq3d | |
20 | 19 | fveq1d | |
21 | 20 | eqeq2d | |
22 | 21 | anbi2d | |
23 | 22 | exbidv | |
24 | 23 | rexbidv | |
25 | 16 24 | orbi12d | |
26 | 25 | iotabidv | |
27 | df-prod | |
|
28 | df-prod | |
|
29 | 26 27 28 | 3eqtr4g | |