Step | Hyp | Ref
| Expression |
1 | | eldifsn 4088 |
. . . . . . 7
    

   |
2 | | simpl 464 |
. . . . . . 7
     |
3 | 1, 2 | sylbi 200 |
. . . . . 6
       |
4 | | simpr 468 |
. . . . . 6
 
   |
5 | | prelpwi 4647 |
. . . . . 6
 
   
   |
6 | 3, 4, 5 | syl2anr 486 |
. . . . 5
  


      
   |
7 | 1 | biimpi 199 |
. . . . . . 7
     
   |
8 | 7 | adantl 473 |
. . . . . 6
  


    
   |
9 | | simpr 468 |
. . . . . . . . 9
     |
10 | 1, 9 | sylbi 200 |
. . . . . . . 8
       |
11 | 10 | adantl 473 |
. . . . . . 7
  


      |
12 | | eqidd 2472 |
. . . . . . 7
  


      
     |
13 | 11, 12 | jca 541 |
. . . . . 6
  


       
      |
14 | | neeq1 2705 |
. . . . . . . . 9
 
   |
15 | | preq1 4042 |
. . . . . . . . . 10
         |
16 | 15 | eqeq2d 2481 |
. . . . . . . . 9
    
  
         |
17 | 14, 16 | anbi12d 725 |
. . . . . . . 8
     
   
           |
18 | 17 | adantl 473 |
. . . . . . 7
  

     
   
           |
19 | 2, 18 | rspcedv 3140 |
. . . . . 6
    
      

           |
20 | 8, 13, 19 | sylc 61 |
. . . . 5
  


    
   
      |
21 | | eqeq1 2475 |
. . . . . . . 8
       
         |
22 | 21 | anbi2d 718 |
. . . . . . 7
     
    
          |
23 | 22 | rexbidv 2892 |
. . . . . 6
     

        
       |
24 | | cusgrafi.p |
. . . . . 6
 

       |
25 | 23, 24 | elrab2 3186 |
. . . . 5
   
    

           |
26 | 6, 20, 25 | sylanbrc 677 |
. . . 4
  


      
  |
27 | 26 | ralrimiva 2809 |
. . 3
 
            |
28 | | preq1 4042 |
. . . . 5
         |
29 | 28 | eleq1d 2533 |
. . . 4
    
      |
30 | 29 | cbvralv 3005 |
. . 3
 
       
           |
31 | 27, 30 | sylibr 217 |
. 2
 
            |
32 | | simpl 464 |
. . . . . . . . . . 11
 
      |
33 | 32 | anim2i 579 |
. . . . . . . . . 10
  
         |
34 | 33 | adantl 473 |
. . . . . . . . 9
        
      
   |
35 | | eldifsn 4088 |
. . . . . . . . 9
    

   |
36 | 34, 35 | sylibr 217 |
. . . . . . . 8
        
            |
37 | | eqeq1 2475 |
. . . . . . . . . . . . . 14
       
         |
38 | 37 | adantl 473 |
. . . . . . . . . . . . 13
 
                 |
39 | 38 | ad2antlr 741 |
. . . . . . . . . . . 12
   
                       |
40 | | vex 3034 |
. . . . . . . . . . . . . 14
 |
41 | | vex 3034 |
. . . . . . . . . . . . . 14
 |
42 | 40, 41 | preqr1 4139 |
. . . . . . . . . . . . 13
         |
43 | 42 | eqcomd 2477 |
. . . . . . . . . . . 12
         |
44 | 39, 43 | syl6bi 236 |
. . . . . . . . . . 11
   
                 |
45 | 44 | adantll 728 |
. . . . . . . . . 10
         
     
    
       |
46 | | preq1 4042 |
. . . . . . . . . . . . . . . 16
         |
47 | 46 | equcoms 1872 |
. . . . . . . . . . . . . . 15
         |
48 | 47 | eqeq2d 2481 |
. . . . . . . . . . . . . 14
    
      |
49 | 48 | biimpcd 232 |
. . . . . . . . . . . . 13
           |
50 | 49 | adantl 473 |
. . . . . . . . . . . 12
 
           |
51 | 50 | adantl 473 |
. . . . . . . . . . 11
  
            |
52 | 51 | ad2antlr 741 |
. . . . . . . . . 10
         
     
    

      |
53 | 45, 52 | impbid 195 |
. . . . . . . . 9
         
     
    
       |
54 | 53 | ralrimiva 2809 |
. . . . . . . 8
        
      
            |
55 | 36, 54 | jca 541 |
. . . . . . 7
        
           
             |
56 | 55 | ex 441 |
. . . . . 6
  

    
         
         
     |
57 | 56 | reximdv2 2855 |
. . . . 5
  

   

   
               
    |
58 | 57 | expimpd 614 |
. . . 4
 
    

                    
    |
59 | | eqeq1 2475 |
. . . . . . 7
    
      |
60 | 59 | anbi2d 718 |
. . . . . 6
  
    
       |
61 | 60 | rexbidv 2892 |
. . . . 5
  

     
       |
62 | 61, 24 | elrab2 3186 |
. . . 4

  

       |
63 | | reu6 3215 |
. . . 4
                         
   |
64 | 58, 62, 63 | 3imtr4g 278 |
. . 3
 
              |
65 | 64 | ralrimiv 2808 |
. 2
 
  
          |
66 | | cusgrafi.f |
. . 3
          |
67 | 66 | f1ompt 6059 |
. 2
        
 
       
 
           |
68 | 31, 65, 67 | sylanbrc 677 |
1
 
           |