Step | Hyp | Ref
| Expression |
1 | | vex 3203 |
. . . . . 6
|
2 | | vex 3203 |
. . . . . 6
|
3 | 1, 2 | pm3.2i 471 |
. . . . 5
|
4 | 3 | a1i 11 |
. . . 4
|
5 | 4 | ssopab2i 5003 |
. . 3
|
6 | 3 | biantru 526 |
. . . . . . . . . 10
|
7 | 6 | exbii 1774 |
. . . . . . . . 9
|
8 | 7 | exbii 1774 |
. . . . . . . 8
|
9 | 8 | abbii 2739 |
. . . . . . 7
|
10 | | ax6ev 1890 |
. . . . . . . . . . . . . . 15
|
11 | | equcom 1945 |
. . . . . . . . . . . . . . . 16
|
12 | 11 | exbii 1774 |
. . . . . . . . . . . . . . 15
|
13 | 10, 12 | mpbi 220 |
. . . . . . . . . . . . . 14
|
14 | | ax6ev 1890 |
. . . . . . . . . . . . . . . . . . 19
|
15 | | equcom 1945 |
. . . . . . . . . . . . . . . . . . . 20
|
16 | 15 | exbii 1774 |
. . . . . . . . . . . . . . . . . . 19
|
17 | 14, 16 | mpbi 220 |
. . . . . . . . . . . . . . . . . 18
|
18 | | idn1 38790 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
19 | | opeq2 4403 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
20 | 18, 19 | e1a 38852 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
21 | | idn2 38838 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
22 | | opeq1 4402 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
23 | 21, 22 | e2 38856 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
24 | | eqeq1 2626 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
25 | 24 | biimprd 238 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
26 | 20, 23, 25 | e12 38951 |
. . . . . . . . . . . . . . . . . . . . . 22
|
27 | | eqeq2 2633 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
28 | 27 | biimpd 219 |
. . . . . . . . . . . . . . . . . . . . . 22
|
29 | 26, 28 | e2 38856 |
. . . . . . . . . . . . . . . . . . . . 21
|
30 | 29 | in2 38830 |
. . . . . . . . . . . . . . . . . . . 20
|
31 | 30 | in1 38787 |
. . . . . . . . . . . . . . . . . . 19
|
32 | 31 | eximi 1762 |
. . . . . . . . . . . . . . . . . 18
|
33 | 17, 32 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
|
34 | 33 | 19.37iv 1911 |
. . . . . . . . . . . . . . . 16
|
35 | | 19.37v 1910 |
. . . . . . . . . . . . . . . . 17
|
36 | 35 | biimpi 206 |
. . . . . . . . . . . . . . . 16
|
37 | 34, 36 | syl 17 |
. . . . . . . . . . . . . . 15
|
38 | 37 | eximi 1762 |
. . . . . . . . . . . . . 14
|
39 | 13, 38 | ax-mp 5 |
. . . . . . . . . . . . 13
|
40 | 39 | 19.37iv 1911 |
. . . . . . . . . . . 12
|
41 | 40 | eximi 1762 |
. . . . . . . . . . 11
|
42 | | 19.9v 1896 |
. . . . . . . . . . . 12
|
43 | 42 | biimpi 206 |
. . . . . . . . . . 11
|
44 | 41, 43 | syl 17 |
. . . . . . . . . 10
|
45 | 44 | eximi 1762 |
. . . . . . . . 9
|
46 | | 19.9v 1896 |
. . . . . . . . . 10
|
47 | 46 | biimpi 206 |
. . . . . . . . 9
|
48 | 45, 47 | syl 17 |
. . . . . . . 8
|
49 | 48 | ss2abi 3674 |
. . . . . . 7
|
50 | 9, 49 | eqsstr3i 3636 |
. . . . . 6
|
51 | | vex 3203 |
. . . . . . . . . . 11
|
52 | | vex 3203 |
. . . . . . . . . . 11
|
53 | 51, 52 | pm3.2i 471 |
. . . . . . . . . 10
|
54 | 53 | biantru 526 |
. . . . . . . . 9
|
55 | 54 | exbii 1774 |
. . . . . . . 8
|
56 | 55 | exbii 1774 |
. . . . . . 7
|
57 | 56 | abbii 2739 |
. . . . . 6
|
58 | 50, 57 | sseqtri 3637 |
. . . . 5
|
59 | | df-opab 4713 |
. . . . 5
|
60 | | df-opab 4713 |
. . . . 5
|
61 | 58, 59, 60 | 3sstr4i 3644 |
. . . 4
|
62 | | df-xp 5120 |
. . . . 5
|
63 | 62 | eqcomi 2631 |
. . . 4
|
64 | 61, 63 | sseqtri 3637 |
. . 3
|
65 | 5, 64 | sstri 3612 |
. 2
|
66 | | df-rel 5121 |
. . 3
|
67 | 66 | biimpri 218 |
. 2
|
68 | 65, 67 | e0a 38999 |
1
|