Step Hyp Ref
Expression
1 vex 3112
. . . 4
2 vex 3112
. . . 4
3 1 , 2 eqvinop 4736
. . 3
4 19.8a 1857
. . . . . . . . 9
5 4 19.23bi 1871
. . . . . . . 8
6 5 ex 434
. . . . . . 7
7 vex 3112
. . . . . . . . 9
8 vex 3112
. . . . . . . . 9
9 7 , 8 opth 4726
. . . . . . . 8
10 9 anbi1i 695
. . . . . . . . . 10
11 10 2exbii 1668
. . . . . . . . 9
12 nfe1 1840
. . . . . . . . . . 11
13 nfae 2056
. . . . . . . . . . . . . 14
14 anass 649
. . . . . . . . . . . . . . 15
15 19.8a 1857
. . . . . . . . . . . . . . . . 17
16 15 a1i 11
. . . . . . . . . . . . . . . 16
17 16 anim2d 565
. . . . . . . . . . . . . . 15
18 14 , 17 syl5bi 217
. . . . . . . . . . . . . 14
19 13 , 18 eximd 1882
. . . . . . . . . . . . 13
20 biidd 237
. . . . . . . . . . . . . 14
21 20 drex1 2069
. . . . . . . . . . . . 13
22 19 , 21 sylibd 214
. . . . . . . . . . . 12
23 14 exbii 1667
. . . . . . . . . . . . . 14
24 19.40 1679
. . . . . . . . . . . . . . 15
25 nfnae 2058
. . . . . . . . . . . . . . . . . 18
26 dveeq2 2042
. . . . . . . . . . . . . . . . . 18
27 25 , 26 nfd 1878
. . . . . . . . . . . . . . . . 17
28 27 19.9d 1892
. . . . . . . . . . . . . . . 16
29 28 anim1d 564
. . . . . . . . . . . . . . 15
30 24 , 29 syl5 32
. . . . . . . . . . . . . 14
31 23 , 30 syl5bi 217
. . . . . . . . . . . . 13
32 19.8a 1857
. . . . . . . . . . . . 13
33 31 , 32 syl6 33
. . . . . . . . . . . 12
34 22 , 33 pm2.61i 164
. . . . . . . . . . 11
35 12 , 34 exlimi 1912
. . . . . . . . . 10
36 euequ1 2288
. . . . . . . . . . . . . 14
37 equcom 1794
. . . . . . . . . . . . . . 15
38 37 eubii 2306
. . . . . . . . . . . . . 14
39 36 , 38 mpbi 208
. . . . . . . . . . . . 13
40 eupick 2358
. . . . . . . . . . . . 13
41 39 , 40 mpan 670
. . . . . . . . . . . 12
42 41 com12 31
. . . . . . . . . . 11
43 euequ1 2288
. . . . . . . . . . . . . 14
44 equcom 1794
. . . . . . . . . . . . . . 15
45 44 eubii 2306
. . . . . . . . . . . . . 14
46 43 , 45 mpbi 208
. . . . . . . . . . . . 13
47 eupick 2358
. . . . . . . . . . . . 13
48 46 , 47 mpan 670
. . . . . . . . . . . 12
49 48 com12 31
. . . . . . . . . . 11
50 42 , 49 sylan9 657
. . . . . . . . . 10
51 35 , 50 syl5 32
. . . . . . . . 9
52 11 , 51 syl5bi 217
. . . . . . . 8
53 9 , 52 sylbi 195
. . . . . . 7
54 6 , 53 impbid 191
. . . . . 6
55 eqeq1 2461
. . . . . . 7
56 55 anbi1d 704
. . . . . . . . 9
57 56 2exbidv 1716
. . . . . . . 8
58 57 bibi2d 318
. . . . . . 7
59 55 , 58 imbi12d 320
. . . . . 6
60 54 , 59 mpbiri 233
. . . . 5
61 60 adantr 465
. . . 4
62 61 exlimivv 1723
. . 3
63 3 , 62 sylbi 195
. 2
64 63 pm2.43i 47
1