Step | Hyp | Ref
| Expression |
1 | | excom 1642 |
. . . . . 6
|
2 | | nfv 1508 |
. . . . . . . . . . 11
|
3 | | cnvoprab.x |
. . . . . . . . . . 11
|
4 | 2, 3 | nfan 1544 |
. . . . . . . . . 10
|
5 | 4 | nfex 1616 |
. . . . . . . . 9
|
6 | | nfv 1508 |
. . . . . . . . . . . 12
|
7 | | cnvoprab.y |
. . . . . . . . . . . 12
|
8 | 6, 7 | nfan 1544 |
. . . . . . . . . . 11
|
9 | 8 | nfex 1616 |
. . . . . . . . . 10
|
10 | | vex 2689 |
. . . . . . . . . . . 12
|
11 | | vex 2689 |
. . . . . . . . . . . 12
|
12 | 10, 11 | opex 4151 |
. . . . . . . . . . 11
|
13 | | opeq1 3705 |
. . . . . . . . . . . . 13
|
14 | 13 | eqeq2d 2151 |
. . . . . . . . . . . 12
|
15 | | cnvoprab.1 |
. . . . . . . . . . . 12
|
16 | 14, 15 | anbi12d 464 |
. . . . . . . . . . 11
|
17 | 12, 16 | spcev 2780 |
. . . . . . . . . 10
|
18 | 9, 17 | exlimi 1573 |
. . . . . . . . 9
|
19 | 5, 18 | exlimi 1573 |
. . . . . . . 8
|
20 | | cnvoprab.2 |
. . . . . . . . . . 11
|
21 | 20 | adantl 275 |
. . . . . . . . . 10
|
22 | | vex 2689 |
. . . . . . . . . . . 12
|
23 | | 1stexg 6065 |
. . . . . . . . . . . 12
|
24 | 22, 23 | ax-mp 5 |
. . . . . . . . . . 11
|
25 | | 2ndexg 6066 |
. . . . . . . . . . . 12
|
26 | 22, 25 | ax-mp 5 |
. . . . . . . . . . 11
|
27 | | eqcom 2141 |
. . . . . . . . . . . . . . 15
|
28 | | eqcom 2141 |
. . . . . . . . . . . . . . 15
|
29 | 27, 28 | anbi12i 455 |
. . . . . . . . . . . . . 14
|
30 | | eqopi 6070 |
. . . . . . . . . . . . . 14
|
31 | 29, 30 | sylan2br 286 |
. . . . . . . . . . . . 13
|
32 | 16 | bicomd 140 |
. . . . . . . . . . . . 13
|
33 | 31, 32 | syl 14 |
. . . . . . . . . . . 12
|
34 | 4, 8, 33 | spc2ed 6130 |
. . . . . . . . . . 11
|
35 | 24, 26, 34 | mpanr12 435 |
. . . . . . . . . 10
|
36 | 21, 35 | mpcom 36 |
. . . . . . . . 9
|
37 | 36 | exlimiv 1577 |
. . . . . . . 8
|
38 | 19, 37 | impbii 125 |
. . . . . . 7
|
39 | 38 | exbii 1584 |
. . . . . 6
|
40 | | exrot3 1668 |
. . . . . 6
|
41 | 1, 39, 40 | 3bitr2ri 208 |
. . . . 5
|
42 | 41 | abbii 2255 |
. . . 4
|
43 | | df-oprab 5778 |
. . . 4
|
44 | | df-opab 3990 |
. . . 4
|
45 | 42, 43, 44 | 3eqtr4ri 2171 |
. . 3
|
46 | 45 | cnveqi 4714 |
. 2
|
47 | | cnvopab 4940 |
. 2
|
48 | 46, 47 | eqtr3i 2162 |
1
|