Step | Hyp | Ref
| Expression |
1 | | ssel 3267 |
. . 3
1c
1c |
2 | | pw1ss1c 4158 |
. . . . 5
1 1c |
3 | 2 | sseli 3269 |
. . . 4
1 1c |
4 | 3 | a1i 10 |
. . 3
1c 1 1c |
5 | | el1c 4139 |
. . . 4
1c
|
6 | | vex 2862 |
. . . . . . . . . 10
|
7 | 6 | snid 3760 |
. . . . . . . . 9
|
8 | | eleq2 2414 |
. . . . . . . . . 10
|
9 | 8 | rspcev 2955 |
. . . . . . . . 9
|
10 | 7, 9 | mpan2 652 |
. . . . . . . 8
|
11 | | el1c 4139 |
. . . . . . . . . . 11
1c
|
12 | | elsn 3748 |
. . . . . . . . . . . . . . 15
|
13 | | sneq 3744 |
. . . . . . . . . . . . . . . 16
|
14 | 13 | eleq1d 2419 |
. . . . . . . . . . . . . . 15
|
15 | 12, 14 | sylbi 187 |
. . . . . . . . . . . . . 14
|
16 | 15 | biimprcd 216 |
. . . . . . . . . . . . 13
|
17 | | eleq1 2413 |
. . . . . . . . . . . . . 14
|
18 | | eleq2 2414 |
. . . . . . . . . . . . . . 15
|
19 | 18 | imbi1d 308 |
. . . . . . . . . . . . . 14
|
20 | 17, 19 | imbi12d 311 |
. . . . . . . . . . . . 13
|
21 | 16, 20 | mpbiri 224 |
. . . . . . . . . . . 12
|
22 | 21 | exlimiv 1634 |
. . . . . . . . . . 11
|
23 | 11, 22 | sylbi 187 |
. . . . . . . . . 10
1c |
24 | 1, 23 | syli 33 |
. . . . . . . . 9
1c |
25 | 24 | rexlimdv 2737 |
. . . . . . . 8
1c |
26 | 10, 25 | impbid2 195 |
. . . . . . 7
1c |
27 | | eluni2 3895 |
. . . . . . 7
|
28 | 26, 27 | syl6bbr 254 |
. . . . . 6
1c |
29 | | eleq1 2413 |
. . . . . . 7
|
30 | | eleq1 2413 |
. . . . . . . 8
1 1 |
31 | | snelpw1 4146 |
. . . . . . . 8
1
|
32 | 30, 31 | syl6bb 252 |
. . . . . . 7
1 |
33 | 29, 32 | bibi12d 312 |
. . . . . 6
1
|
34 | 28, 33 | syl5ibrcom 213 |
. . . . 5
1c 1 |
35 | 34 | exlimdv 1636 |
. . . 4
1c
1 |
36 | 5, 35 | syl5bi 208 |
. . 3
1c 1c
1 |
37 | 1, 4, 36 | pm5.21ndd 343 |
. 2
1c
1 |
38 | 37 | eqrdv 2351 |
1
1c 1 |