Step | Hyp | Ref
| Expression |
1 | | anandir 559 |
. . . . . . . 8
   
  
     
      |
2 | 1 | exbii 1548 |
. . . . . . 7
    
           
      |
3 | | 19.40 1574 |
. . . . . . 7
        
             
      |
4 | 2, 3 | sylbi 120 |
. . . . . 6
    
                    |
5 | | nfv 1473 |
. . . . . . . . . . 11
    |
6 | | nfe1 1437 |
. . . . . . . . . . 11
         |
7 | 5, 6 | nfan 1509 |
. . . . . . . . . 10
  
     
   |
8 | | funmo 5064 |
. . . . . . . . . . . . . 14
 
      |
9 | | vex 2636 |
. . . . . . . . . . . . . . . 16
 |
10 | | vex 2636 |
. . . . . . . . . . . . . . . 16
 |
11 | 9, 10 | brcnv 4650 |
. . . . . . . . . . . . . . 15
   
    |
12 | 11 | mobii 1992 |
. . . . . . . . . . . . . 14
          |
13 | 8, 12 | sylib 121 |
. . . . . . . . . . . . 13
 
     |
14 | | mopick 2033 |
. . . . . . . . . . . . 13
              
   |
15 | 13, 14 | sylan 278 |
. . . . . . . . . . . 12
            
   |
16 | 15 | con2d 592 |
. . . . . . . . . . 11
                |
17 | | imnan 662 |
. . . . . . . . . . 11
           |
18 | 16, 17 | sylib 121 |
. . . . . . . . . 10
                |
19 | 7, 18 | alrimi 1467 |
. . . . . . . . 9
          
      |
20 | 19 | ex 114 |
. . . . . . . 8
 
               |
21 | | exancom 1551 |
. . . . . . . 8
      
        |
22 | | alnex 1440 |
. . . . . . . 8
     
        |
23 | 20, 21, 22 | 3imtr3g 203 |
. . . . . . 7
 
   
            |
24 | 23 | anim2d 331 |
. . . . . 6
 
          
                     |
25 | 4, 24 | syl5 32 |
. . . . 5
 
    
                     |
26 | | df-rex 2376 |
. . . . . 6
      
          |
27 | | eldif 3022 |
. . . . . . . 8
  

   |
28 | 27 | anbi1i 447 |
. . . . . . 7
      
 

     |
29 | 28 | exbii 1548 |
. . . . . 6
     
  
          |
30 | 26, 29 | bitri 183 |
. . . . 5
      
          |
31 | | df-rex 2376 |
. . . . . 6
   
        |
32 | | df-rex 2376 |
. . . . . . 7
   
        |
33 | 32 | notbii 632 |
. . . . . 6
   
        |
34 | 31, 33 | anbi12i 449 |
. . . . 5
        
                |
35 | 25, 30, 34 | 3imtr4g 204 |
. . . 4
 
        
         |
36 | 35 | ss2abdv 3109 |
. . 3
 
       
  
 

      |
37 | | dfima2 4809 |
. . 3
       
       |
38 | | dfima2 4809 |
. . . . 5
     
    |
39 | | dfima2 4809 |
. . . . 5
     
    |
40 | 38, 39 | difeq12i 3131 |
. . . 4
                 
     |
41 | | difab 3284 |
. . . 4
  
    
               |
42 | 40, 41 | eqtri 2115 |
. . 3
                     |
43 | 36, 37, 42 | 3sstr4g 3082 |
. 2
 
                  |
44 | | imadiflem 5127 |
. . 3
                 |
45 | 44 | a1i 9 |
. 2
 
                  |
46 | 43, 45 | eqssd 3056 |
1
 
                  |