Step | Hyp | Ref
| Expression |
1 | | biidd 241 |
. . . . . . 7
  


  

    |
2 | 1 | cbvralv 3021 |
. . . . . 6
 



   

   |
3 | | eleq1 2519 |
. . . . . . . . . 10
 
   |
4 | 3 | anbi2d 711 |
. . . . . . . . 9
  
      |
5 | 4 | rexbidv 2903 |
. . . . . . . 8
  

  
    |
6 | 5 | cbvreuv 3023 |
. . . . . . 7
  

  

   |
7 | 6 | ralbii 2821 |
. . . . . 6
 



   

   |
8 | 2, 7 | bitri 253 |
. . . . 5
 



   

   |
9 | 8 | ralbii 2821 |
. . . 4
 




  



   |
10 | | eleq1 2519 |
. . . . . . . . 9
 
   |
11 | 10 | anbi1d 712 |
. . . . . . . 8
  
      |
12 | 11 | rexbidv 2903 |
. . . . . . 7
  

  
    |
13 | 12 | reueqd 2999 |
. . . . . 6
  


  

    |
14 | 13 | raleqbi1dv 2997 |
. . . . 5
  



  


    |
15 | 14 | cbvralv 3021 |
. . . 4
 




  



   |
16 | | eleq1 2519 |
. . . . . . . . 9
 
   |
17 | 16 | anbi1d 712 |
. . . . . . . 8
  
      |
18 | 17 | rexbidv 2903 |
. . . . . . 7
  

  
    |
19 | 18 | reueqd 2999 |
. . . . . 6
  


  

    |
20 | 19 | raleqbi1dv 2997 |
. . . . 5
  



  


    |
21 | 20 | cbvralv 3021 |
. . . 4
 




  



   |
22 | 9, 15, 21 | 3bitr4i 281 |
. . 3
 




  



   |
23 | 22 | exbii 1720 |
. 2
        
  




   |
24 | | 19.21v 1788 |
. . . . . 6
   

          
    

           


 
     |
25 | | impexp 448 |
. . . . . . . 8
  

          
   

           
       |
26 | | bi2.04 363 |
. . . . . . . 8
           


 
             


 
     |
27 | 25, 26 | bitri 253 |
. . . . . . 7
  

          
   

           
       |
28 | 27 | albii 1693 |
. . . . . 6
                
   
            


 
     |
29 | | df-eu 2305 |
. . . . . . . . . . 11
    

 
      

     |
30 | | df-reu 2746 |
. . . . . . . . . . 11
  

    

    |
31 | | 19.42v 1836 |
. . . . . . . . . . . . . . 15
     
  

         |
32 | | an42 835 |
. . . . . . . . . . . . . . . . 17
  


 
 
 
    |
33 | | anass 655 |
. . . . . . . . . . . . . . . . 17
  


 

 
     |
34 | 32, 33 | bitr3i 255 |
. . . . . . . . . . . . . . . 16
  


 

 
     |
35 | 34 | exbii 1720 |
. . . . . . . . . . . . . . 15
      
      
     |
36 | | df-rex 2745 |
. . . . . . . . . . . . . . . . 17
  
         |
37 | | eleq1 2519 |
. . . . . . . . . . . . . . . . . . 19
 
   |
38 | | eleq2 2520 |
. . . . . . . . . . . . . . . . . . . 20
 
   |
39 | | eleq2 2520 |
. . . . . . . . . . . . . . . . . . . 20
 
   |
40 | 38, 39 | anbi12d 718 |
. . . . . . . . . . . . . . . . . . 19
  
      |
41 | 37, 40 | anbi12d 718 |
. . . . . . . . . . . . . . . . . 18
     


     |
42 | 41 | cbvexv 2119 |
. . . . . . . . . . . . . . . . 17
      
        |
43 | 36, 42 | bitri 253 |
. . . . . . . . . . . . . . . 16
  
         |
44 | 43 | anbi2i 701 |
. . . . . . . . . . . . . . 15
   
            |
45 | 31, 35, 44 | 3bitr4i 281 |
. . . . . . . . . . . . . 14
      
   

    |
46 | 45 | bibi1i 316 |
. . . . . . . . . . . . 13
     
 
 

   
     |
47 | 46 | albii 1693 |
. . . . . . . . . . . 12
         
        
     |
48 | 47 | exbii 1720 |
. . . . . . . . . . 11
         
 
 

      

     |
49 | 29, 30, 48 | 3bitr4i 281 |
. . . . . . . . . 10
  

         
 
 
   |
50 | 49 | imbi2i 314 |
. . . . . . . . 9
  


 

          
      |
51 | 50 | albii 1693 |
. . . . . . . 8
   



 
           


 
    |
52 | | df-ral 2744 |
. . . . . . . 8
 



   



    |
53 | | nfv 1763 |
. . . . . . . . 9
           


 
   |
54 | | nfv 1763 |
. . . . . . . . . 10
  |
55 | | nfa1 1981 |
. . . . . . . . . . 11
          
    |
56 | 55 | nfex 2033 |
. . . . . . . . . 10
          


 
  |
57 | 54, 56 | nfim 2005 |
. . . . . . . . 9
           


 
   |
58 | | eleq1 2519 |
. . . . . . . . . 10
 
   |
59 | 58 | imbi1d 319 |
. . . . . . . . 9
           


 
 

          
       |
60 | 53, 57, 59 | cbval 2116 |
. . . . . . . 8
   
          
   
           


 
    |
61 | 51, 52, 60 | 3bitr4i 281 |
. . . . . . 7
 



   
          
      |
62 | 61 | imbi2i 314 |
. . . . . 6
  



 

           


 
     |
63 | 24, 28, 62 | 3bitr4i 281 |
. . . . 5
                
   





    |
64 | 63 | albii 1693 |
. . . 4
      
         


 
 
    


    |
65 | | alcom 1925 |
. . . 4
      
         


 
 
                 
      |
66 | | df-ral 2744 |
. . . 4
 




   




    |
67 | 64, 65, 66 | 3bitr4ri 282 |
. . 3
 




      

          
      |
68 | 67 | exbii 1720 |
. 2
        
       

          
      |
69 | 23, 68 | bitri 253 |
1
        
       

          
      |