Step | Hyp | Ref
| Expression |
1 | | elisset 3043 |
. . . 4
    |
2 | | eleq2 2538 |
. . . . . . 7
         |
3 | 2 | abbidv 2589 |
. . . . . 6
    
  
   |
4 | | eleq1 2537 |
. . . . . . 7
   
         
  
    |
5 | 4 | biimpd 212 |
. . . . . 6
   
         
   
   |
6 | 3, 5 | syl 17 |
. . . . 5
  
     
    |
7 | 6 | eximi 1715 |
. . . 4
       

   
   |
8 | 1, 7 | syl 17 |
. . 3
       
   
   |
9 | | 19.35 1748 |
. . . . . 6
       
   
       
     
   |
10 | 9 | biimpi 199 |
. . . . 5
       
   
      

  
  
   |
11 | 10 | com12 31 |
. . . 4
             

   
      
   |
12 | | ax-rep 4508 |
. . . . . . . 8
           
        
      |
13 | | 19.3v 1821 |
. . . . . . . . . . 11
 
 
    |
14 | 13 | sbbii 1812 |
. . . . . . . . . . 11
   ![] ]](rbrack.gif)   
  ![] ]](rbrack.gif)     |
15 | | sbsbc 3259 |
. . . . . . . . . . . . . 14
   ![] ]](rbrack.gif)     ![]. ].](_drbrack.gif)
    |
16 | | vex 3034 |
. . . . . . . . . . . . . . 15
 |
17 | | sbceq2g 3783 |
. . . . . . . . . . . . . . 15
  
 ![]. ].](_drbrack.gif)
 
  ![]_ ]_](_urbrack.gif)      |
18 | 16, 17 | ax-mp 5 |
. . . . . . . . . . . . . 14
   ![]. ].](_drbrack.gif)  
  ![]_ ]_](_urbrack.gif)     |
19 | 15, 18 | bitri 257 |
. . . . . . . . . . . . 13
   ![] ]](rbrack.gif)  
  ![]_ ]_](_urbrack.gif)     |
20 | | bj-csbsn 31574 |
. . . . . . . . . . . . . 14
  ![]_ ]_](_urbrack.gif)      |
21 | 20 | eqeq2i 2483 |
. . . . . . . . . . . . 13
   ![]_ ]_](_urbrack.gif)       |
22 | 19, 21 | bitri 257 |
. . . . . . . . . . . 12
   ![] ]](rbrack.gif)  
    |
23 | | eqtr2 2491 |
. . . . . . . . . . . . 13
             |
24 | | vex 3034 |
. . . . . . . . . . . . . 14
 |
25 | 24 | sneqr 4131 |
. . . . . . . . . . . . 13
       |
26 | 23, 25 | syl 17 |
. . . . . . . . . . . 12
         |
27 | 22, 26 | sylan2b 483 |
. . . . . . . . . . 11
      ![] ]](rbrack.gif)      |
28 | 13, 14, 27 | syl2anb 487 |
. . . . . . . . . 10
       ![] ]](rbrack.gif)       |
29 | 28 | gen2 1678 |
. . . . . . . . 9
      
    ![] ]](rbrack.gif)       |
30 | | nfa1 1999 |
. . . . . . . . . 10
      |
31 | 30 | mo 2357 |
. . . . . . . . 9
         
      
    ![] ]](rbrack.gif)        |
32 | 29, 31 | mpbir 214 |
. . . . . . . 8
     
    |
33 | 12, 32 | mpg 1679 |
. . . . . . 7
        
     |
34 | | bj-sbel1 31575 |
. . . . . . . . . . . 12
   ![] ]](rbrack.gif)     ![]_ ]_](_urbrack.gif)     |
35 | | bj-csbsn 31574 |
. . . . . . . . . . . . 13
  ![]_ ]_](_urbrack.gif)  
   |
36 | 35 | eleq1i 2540 |
. . . . . . . . . . . 12
   ![]_ ]_](_urbrack.gif)       |
37 | 34, 36 | bitri 257 |
. . . . . . . . . . 11
   ![] ]](rbrack.gif)       |
38 | | df-clab 2458 |
. . . . . . . . . . 11
    
  ![] ]](rbrack.gif)     |
39 | 13 | anbi2i 708 |
. . . . . . . . . . . . . 14
     

     |
40 | | eleq1a 2544 |
. . . . . . . . . . . . . . . . . 18
         |
41 | 40 | com12 31 |
. . . . . . . . . . . . . . . . 17
   
 
   |
42 | 41 | eqcoms 2479 |
. . . . . . . . . . . . . . . 16
   
 
   |
43 | 42 | imdistanri 705 |
. . . . . . . . . . . . . . 15
 
           |
44 | | eleq1a 2544 |
. . . . . . . . . . . . . . . 16
         |
45 | 44 | impac 633 |
. . . . . . . . . . . . . . 15
             |
46 | 43, 45 | impbii 192 |
. . . . . . . . . . . . . 14
 
  
        |
47 | 39, 46 | bitri 257 |
. . . . . . . . . . . . 13
     
        |
48 | 47 | exbii 1726 |
. . . . . . . . . . . 12
    
  
          |
49 | | snex 4641 |
. . . . . . . . . . . . . 14
   |
50 | 49 | isseti 3037 |
. . . . . . . . . . . . 13

   |
51 | | 19.42v 1842 |
. . . . . . . . . . . . 13
     
  
         |
52 | 50, 51 | mpbiran2 933 |
. . . . . . . . . . . 12
     
  
 
  |
53 | 48, 52 | bitri 257 |
. . . . . . . . . . 11
    
  
 
  |
54 | 37, 38, 53 | 3bitr4ri 286 |
. . . . . . . . . 10
    
  
  
   |
55 | 54 | bibi2i 320 |
. . . . . . . . 9
 
       

  
    |
56 | 55 | albii 1699 |
. . . . . . . 8
       
         
    |
57 | 56 | exbii 1726 |
. . . . . . 7
     
       
       
    |
58 | 33, 57 | mpbi 213 |
. . . . . 6
       
   |
59 | | dfcleq 2465 |
. . . . . . 7
    
  
  
    |
60 | 59 | exbii 1726 |
. . . . . 6
    
     
  
    |
61 | 58, 60 | mpbir 214 |
. . . . 5
      |
62 | 61 | issetri 3038 |
. . . 4
   
 |
63 | 11, 62 | mpg 1679 |
. . 3
       
   
      
  |
64 | 8, 63 | syl 17 |
. 2
   
  
  |
65 | | ax5e 1768 |
. 2
      
   
  |
66 | 64, 65 | syl 17 |
1
    
  |