Step | Hyp | Ref
| Expression |
1 | | elex 2749 |
. . . . . . . . . . . 12
   |
2 | | prid2g 3698 |
. . . . . . . . . . . . 13
      |
3 | | eldif 3139 |
. . . . . . . . . . . . . . 15
      
      |
4 | | pm3.4 333 |
. . . . . . . . . . . . . . 15
 
      
    |
5 | 3, 4 | sylbi 121 |
. . . . . . . . . . . . . 14
     

      |
6 | 5 | com12 30 |
. . . . . . . . . . . . 13
 
    
      |
7 | 2, 6 | mt2d 625 |
. . . . . . . . . . . 12

       |
8 | 1, 7 | syl 14 |
. . . . . . . . . . 11

       |
9 | 8 | ad2antlr 489 |
. . . . . . . . . 10
  

         

      |
10 | | simp1r 1022 |
. . . . . . . . . . . 12
  

        
   |
11 | | eleq1 2240 |
. . . . . . . . . . . . . . . . 17
 
   |
12 | | eleq1 2240 |
. . . . . . . . . . . . . . . . 17
      

       |
13 | 11, 12 | imbi12d 234 |
. . . . . . . . . . . . . . . 16
        

  
      |
14 | 13 | spcgv 2825 |
. . . . . . . . . . . . . . 15
    

     

        |
15 | 14 | pm2.43b 52 |
. . . . . . . . . . . . . 14
   

     

       |
16 | 15 | 3ad2ant2 1019 |
. . . . . . . . . . . . 13
  

        
          |
17 | | eleq2 2241 |
. . . . . . . . . . . . . . 15
 
   |
18 | 17 | imbi1d 231 |
. . . . . . . . . . . . . 14
        

  
      |
19 | 18 | 3ad2ant3 1020 |
. . . . . . . . . . . . 13
  

        
  

               |
20 | 16, 19 | mpbid 147 |
. . . . . . . . . . . 12
  

        
          |
21 | 10, 20 | mpd 13 |
. . . . . . . . . . 11
  

        
        |
22 | 21 | 3expia 1205 |
. . . . . . . . . 10
  

          

       |
23 | 9, 22 | mtod 663 |
. . . . . . . . 9
  

         
  |
24 | | elex 2749 |
. . . . . . . . . . . . 13
   |
25 | | prid1g 3697 |
. . . . . . . . . . . . . 14
      |
26 | | eldif 3139 |
. . . . . . . . . . . . . . . 16
      
      |
27 | | pm3.4 333 |
. . . . . . . . . . . . . . . 16
 
      
    |
28 | 26, 27 | sylbi 121 |
. . . . . . . . . . . . . . 15
     

      |
29 | 28 | com12 30 |
. . . . . . . . . . . . . 14
 
    
      |
30 | 25, 29 | mt2d 625 |
. . . . . . . . . . . . 13

       |
31 | 24, 30 | syl 14 |
. . . . . . . . . . . 12

       |
32 | 31 | adantr 276 |
. . . . . . . . . . 11
 
        |
33 | 32 | adantr 276 |
. . . . . . . . . 10
  

         

      |
34 | | simp1l 1021 |
. . . . . . . . . . . 12
  

        
   |
35 | | eleq1 2240 |
. . . . . . . . . . . . . . . . 17
 
   |
36 | | eleq1 2240 |
. . . . . . . . . . . . . . . . 17
      

       |
37 | 35, 36 | imbi12d 234 |
. . . . . . . . . . . . . . . 16
        

  
      |
38 | 37 | spcgv 2825 |
. . . . . . . . . . . . . . 15
    

     

        |
39 | 38 | pm2.43b 52 |
. . . . . . . . . . . . . 14
   

     

       |
40 | 39 | 3ad2ant2 1019 |
. . . . . . . . . . . . 13
  

        
          |
41 | | eleq2 2241 |
. . . . . . . . . . . . . . 15
 
   |
42 | 41 | imbi1d 231 |
. . . . . . . . . . . . . 14
        

  
      |
43 | 42 | 3ad2ant3 1020 |
. . . . . . . . . . . . 13
  

        
  

               |
44 | 40, 43 | mpbid 147 |
. . . . . . . . . . . 12
  

        
          |
45 | 34, 44 | mpd 13 |
. . . . . . . . . . 11
  

        
        |
46 | 45 | 3expia 1205 |
. . . . . . . . . 10
  

          

       |
47 | 33, 46 | mtod 663 |
. . . . . . . . 9
  

         
  |
48 | | ioran 752 |
. . . . . . . . 9
   
   |
49 | 23, 47, 48 | sylanbrc 417 |
. . . . . . . 8
  

         

   |
50 | | vex 2741 |
. . . . . . . . . 10
 |
51 | | eldif 3139 |
. . . . . . . . . 10
      
      |
52 | 50, 51 | mpbiran 940 |
. . . . . . . . 9
     
     |
53 | 50 | elpr 3614 |
. . . . . . . . 9
   
    |
54 | 52, 53 | xchbinx 682 |
. . . . . . . 8
     

   |
55 | 49, 54 | sylibr 134 |
. . . . . . 7
  

                 |
56 | 55 | ex 115 |
. . . . . 6
 
          
        |
57 | 56 | alrimiv 1874 |
. . . . 5
 
      

             |
58 | | df-ral 2460 |
. . . . . . . 8
 
  ![] ]](rbrack.gif)     
     ![] ]](rbrack.gif)
        |
59 | | clelsb1 2282 |
. . . . . . . . . 10
   ![] ]](rbrack.gif)     

      |
60 | 59 | imbi2i 226 |
. . . . . . . . 9
    ![] ]](rbrack.gif)
     

  
     |
61 | 60 | albii 1470 |
. . . . . . . 8
   
  ![] ]](rbrack.gif)   
  
           |
62 | 58, 61 | bitri 184 |
. . . . . . 7
 
  ![] ]](rbrack.gif)     
           |
63 | 62 | imbi1i 238 |
. . . . . 6
     ![] ]](rbrack.gif)
       
  
   

             |
64 | 63 | albii 1470 |
. . . . 5
    
  ![] ]](rbrack.gif)   
 

                
        |
65 | 57, 64 | sylibr 134 |
. . . 4
 
    
  ![] ]](rbrack.gif)        
     |
66 | | ax-setind 4537 |
. . . 4
    
  ![] ]](rbrack.gif)   
 

        
    |
67 | 65, 66 | syl 14 |
. . 3
 
    
    |
68 | | eleq1 2240 |
. . . . 5
      

       |
69 | 68 | spcgv 2825 |
. . . 4
  

   
        |
70 | 69 | adantr 276 |
. . 3
 
       

       |
71 | 67, 70 | mpd 13 |
. 2
 
        |
72 | 71, 32 | pm2.65i 639 |
1

  |