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 19.8a 1857
. . . . . . . . . . . . . . . 16
14 13 anim2i 569
. . . . . . . . . . . . . . 15
15 14 anassrs 648
. . . . . . . . . . . . . 14
16 15 eximi 1656
. . . . . . . . . . . . 13
17 biidd 237
. . . . . . . . . . . . . 14
18 17 drex1 2069
. . . . . . . . . . . . 13
19 16 , 18 syl5ib 219
. . . . . . . . . . . 12
20 anass 649
. . . . . . . . . . . . . . 15
21 20 exbii 1667
. . . . . . . . . . . . . 14
22 19.40 1679
. . . . . . . . . . . . . . 15
23 nfeqf2 2041
. . . . . . . . . . . . . . . . 17
24 23 19.9d 1892
. . . . . . . . . . . . . . . 16
25 24 anim1d 564
. . . . . . . . . . . . . . 15
26 22 , 25 syl5 32
. . . . . . . . . . . . . 14
27 21 , 26 syl5bi 217
. . . . . . . . . . . . 13
28 19.8a 1857
. . . . . . . . . . . . 13
29 27 , 28 syl6 33
. . . . . . . . . . . 12
30 19 , 29 pm2.61i 164
. . . . . . . . . . 11
31 12 , 30 exlimi 1912
. . . . . . . . . 10
32 euequ1 2288
. . . . . . . . . . . . . 14
33 equcom 1794
. . . . . . . . . . . . . . 15
34 33 eubii 2306
. . . . . . . . . . . . . 14
35 32 , 34 mpbi 208
. . . . . . . . . . . . 13
36 eupick 2358
. . . . . . . . . . . . 13
37 35 , 36 mpan 670
. . . . . . . . . . . 12
38 37 com12 31
. . . . . . . . . . 11
39 euequ1 2288
. . . . . . . . . . . . . 14
40 equcom 1794
. . . . . . . . . . . . . . 15
41 40 eubii 2306
. . . . . . . . . . . . . 14
42 39 , 41 mpbi 208
. . . . . . . . . . . . 13
43 eupick 2358
. . . . . . . . . . . . 13
44 42 , 43 mpan 670
. . . . . . . . . . . 12
45 44 com12 31
. . . . . . . . . . 11
46 38 , 45 sylan9 657
. . . . . . . . . 10
47 31 , 46 syl5 32
. . . . . . . . 9
48 11 , 47 syl5bi 217
. . . . . . . 8
49 9 , 48 sylbi 195
. . . . . . 7
50 6 , 49 impbid 191
. . . . . 6
51 eqeq1 2461
. . . . . . 7
52 51 anbi1d 704
. . . . . . . . 9
53 52 2exbidv 1716
. . . . . . . 8
54 53 bibi2d 318
. . . . . . 7
55 51 , 54 imbi12d 320
. . . . . 6
56 50 , 55 mpbiri 233
. . . . 5
57 56 adantr 465
. . . 4
58 57 exlimivv 1723
. . 3
59 3 , 58 sylbi 195
. 2
60 59 pm2.43i 47
1