Step | Hyp | Ref
| Expression |
1 | | excom 1657 |
. . . . . 6
|
2 | | nfv 1521 |
. . . . . . . . . . 11
|
3 | | cnvoprab.x |
. . . . . . . . . . 11
|
4 | 2, 3 | nfan 1558 |
. . . . . . . . . 10
|
5 | 4 | nfex 1630 |
. . . . . . . . 9
|
6 | | nfv 1521 |
. . . . . . . . . . . 12
|
7 | | cnvoprab.y |
. . . . . . . . . . . 12
|
8 | 6, 7 | nfan 1558 |
. . . . . . . . . . 11
|
9 | 8 | nfex 1630 |
. . . . . . . . . 10
|
10 | | vex 2733 |
. . . . . . . . . . . 12
|
11 | | vex 2733 |
. . . . . . . . . . . 12
|
12 | 10, 11 | opex 4212 |
. . . . . . . . . . 11
|
13 | | opeq1 3763 |
. . . . . . . . . . . . 13
|
14 | 13 | eqeq2d 2182 |
. . . . . . . . . . . 12
|
15 | | cnvoprab.1 |
. . . . . . . . . . . 12
|
16 | 14, 15 | anbi12d 470 |
. . . . . . . . . . 11
|
17 | 12, 16 | spcev 2825 |
. . . . . . . . . 10
|
18 | 9, 17 | exlimi 1587 |
. . . . . . . . 9
|
19 | 5, 18 | exlimi 1587 |
. . . . . . . 8
|
20 | | cnvoprab.2 |
. . . . . . . . . . 11
|
21 | 20 | adantl 275 |
. . . . . . . . . 10
|
22 | | vex 2733 |
. . . . . . . . . . . 12
|
23 | | 1stexg 6144 |
. . . . . . . . . . . 12
|
24 | 22, 23 | ax-mp 5 |
. . . . . . . . . . 11
|
25 | | 2ndexg 6145 |
. . . . . . . . . . . 12
|
26 | 22, 25 | ax-mp 5 |
. . . . . . . . . . 11
|
27 | | eqcom 2172 |
. . . . . . . . . . . . . . 15
|
28 | | eqcom 2172 |
. . . . . . . . . . . . . . 15
|
29 | 27, 28 | anbi12i 457 |
. . . . . . . . . . . . . 14
|
30 | | eqopi 6149 |
. . . . . . . . . . . . . 14
|
31 | 29, 30 | sylan2br 286 |
. . . . . . . . . . . . 13
|
32 | 16 | bicomd 140 |
. . . . . . . . . . . . 13
|
33 | 31, 32 | syl 14 |
. . . . . . . . . . . 12
|
34 | 4, 8, 33 | spc2ed 6210 |
. . . . . . . . . . 11
|
35 | 24, 26, 34 | mpanr12 437 |
. . . . . . . . . 10
|
36 | 21, 35 | mpcom 36 |
. . . . . . . . 9
|
37 | 36 | exlimiv 1591 |
. . . . . . . 8
|
38 | 19, 37 | impbii 125 |
. . . . . . 7
|
39 | 38 | exbii 1598 |
. . . . . 6
|
40 | | exrot3 1683 |
. . . . . 6
|
41 | 1, 39, 40 | 3bitr2ri 208 |
. . . . 5
|
42 | 41 | abbii 2286 |
. . . 4
|
43 | | df-oprab 5855 |
. . . 4
|
44 | | df-opab 4049 |
. . . 4
|
45 | 42, 43, 44 | 3eqtr4ri 2202 |
. . 3
|
46 | 45 | cnveqi 4784 |
. 2
|
47 | | cnvopab 5010 |
. 2
|
48 | 46, 47 | eqtr3i 2193 |
1
|