Step | Hyp | Ref
| Expression |
1 | | ralnex 2834 |
. . . . 5
 

   ![]. ].](_drbrack.gif)
      ![]. ].](_drbrack.gif)   |
2 | | vex 3034 |
. . . . . . . 8
 |
3 | | sbcng 3296 |
. . . . . . . 8
  

  ![]. ].](_drbrack.gif)    |
4 | 2, 3 | ax-mp 5 |
. . . . . . 7
     ![]. ].](_drbrack.gif)   |
5 | 4 | bicomi 207 |
. . . . . 6
   ![]. ].](_drbrack.gif)     |
6 | 5 | ralbii 2823 |
. . . . 5
 

   ![]. ].](_drbrack.gif)
        |
7 | 1, 6 | bitr3i 259 |
. . . 4
       ![]. ].](_drbrack.gif)
        |
8 | | df-rab 2765 |
. . . . . . 7

      |
9 | 8 | eleq2i 2541 |
. . . . . 6
         |
10 | | df-sbc 3256 |
. . . . . . 7
   ![]. ].](_drbrack.gif)  
      |
11 | | sbcan 3298 |
. . . . . . . 8
   ![]. ].](_drbrack.gif)  
   ![]. ].](_drbrack.gif)
     |
12 | | sbcel1v 3314 |
. . . . . . . . 9
   ![]. ].](_drbrack.gif)
  |
13 | 12 | anbi1i 709 |
. . . . . . . 8
    ![]. ].](_drbrack.gif)
  

     |
14 | 11, 13 | bitri 257 |
. . . . . . 7
   ![]. ].](_drbrack.gif)  

     |
15 | 10, 14 | bitr3i 259 |
. . . . . 6
           |
16 | 9, 15 | bitri 257 |
. . . . 5
         |
17 | 16 | simprbi 471 |
. . . 4
       |
18 | 7, 17 | mprgbir 2771 |
. . 3


    ![]. ].](_drbrack.gif)  |
19 | | bnj110.1 |
. . . . . . . . 9
 |
20 | 19 | rabex 4550 |
. . . . . . . 8

  |
21 | 20 | biantrur 514 |
. . . . . . 7

      |
22 | | rexnal 2836 |
. . . . . . . 8
     |
23 | | rabn0 3755 |
. . . . . . . . 9
  

  |
24 | | ssrab2 3500 |
. . . . . . . . . 10


 |
25 | 24 | biantrur 514 |
. . . . . . . . 9
  
        |
26 | 23, 25 | bitr3i 259 |
. . . . . . . 8
          |
27 | 22, 26 | bitr3i 259 |
. . . . . . 7
          |
28 | | fri 4801 |
. . . . . . 7
    
  
     

         |
29 | 21, 27, 28 | syl2anb 487 |
. . . . . 6
   
    

     |
30 | | eqid 2471 |
. . . . . . . 8

 
  |
31 | 30 | bnj23 29596 |
. . . . . . 7
 

  

     ![]. ].](_drbrack.gif)    |
32 | | df-ral 2761 |
. . . . . . . . . 10
 
   
 ![]. ].](_drbrack.gif) 
        ![]. ].](_drbrack.gif)     |
33 | 32 | sbcbii 3311 |
. . . . . . . . 9
   ![]. ].](_drbrack.gif) 
   
 ![]. ].](_drbrack.gif) 
  ![]. ].](_drbrack.gif)         ![]. ].](_drbrack.gif)     |
34 | | sbcal 3305 |
. . . . . . . . . 10
   ![]. ].](_drbrack.gif)   
  
  ![]. ].](_drbrack.gif)       ![]. ].](_drbrack.gif)     
 ![]. ].](_drbrack.gif)     |
35 | | sbcimg 3297 |
. . . . . . . . . . . . 13
  
 ![]. ].](_drbrack.gif)       ![]. ].](_drbrack.gif)  
   ![]. ].](_drbrack.gif)
  ![]. ].](_drbrack.gif)      ![]. ].](_drbrack.gif)      |
36 | 2, 35 | ax-mp 5 |
. . . . . . . . . . . 12
   ![]. ].](_drbrack.gif)       ![]. ].](_drbrack.gif)  
   ![]. ].](_drbrack.gif)
  ![]. ].](_drbrack.gif)      ![]. ].](_drbrack.gif)     |
37 | | nfv 1769 |
. . . . . . . . . . . . . . 15

 |
38 | 37 | sbcgf 3319 |
. . . . . . . . . . . . . 14
  
 ![]. ].](_drbrack.gif)
   |
39 | 2, 38 | ax-mp 5 |
. . . . . . . . . . . . 13
   ![]. ].](_drbrack.gif)
  |
40 | | sbcimg 3297 |
. . . . . . . . . . . . . . 15
  
 ![]. ].](_drbrack.gif)      ![]. ].](_drbrack.gif) 
   ![]. ].](_drbrack.gif)  
  ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)     |
41 | 2, 40 | ax-mp 5 |
. . . . . . . . . . . . . 14
   ![]. ].](_drbrack.gif)    
 ![]. ].](_drbrack.gif) 
   ![]. ].](_drbrack.gif)  
  ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)    |
42 | | sbcbr2g 4451 |
. . . . . . . . . . . . . . . . 17
  
 ![]. ].](_drbrack.gif)  
  
 ![]_ ]_](_urbrack.gif)    |
43 | 2, 42 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
   ![]. ].](_drbrack.gif)  
    ![]_ ]_](_urbrack.gif)   |
44 | | csbvarg 3796 |
. . . . . . . . . . . . . . . . . 18
   ![]_ ]_](_urbrack.gif)   |
45 | 2, 44 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
  ![]_ ]_](_urbrack.gif)  |
46 | 45 | breq2i 4403 |
. . . . . . . . . . . . . . . 16
     ![]_ ]_](_urbrack.gif)
    |
47 | 43, 46 | bitri 257 |
. . . . . . . . . . . . . . 15
   ![]. ].](_drbrack.gif)  
    |
48 | | nfsbc1v 3275 |
. . . . . . . . . . . . . . . . 17
  
 ![]. ].](_drbrack.gif)  |
49 | 48 | sbcgf 3319 |
. . . . . . . . . . . . . . . 16
  
 ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)    |
50 | 2, 49 | ax-mp 5 |
. . . . . . . . . . . . . . 15
   ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)
  ![]. ].](_drbrack.gif)   |
51 | 47, 50 | imbi12i 333 |
. . . . . . . . . . . . . 14
    ![]. ].](_drbrack.gif)   
 ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif) 
     ![]. ].](_drbrack.gif)    |
52 | 41, 51 | bitri 257 |
. . . . . . . . . . . . 13
   ![]. ].](_drbrack.gif)    
 ![]. ].](_drbrack.gif) 
     ![]. ].](_drbrack.gif)    |
53 | 39, 52 | imbi12i 333 |
. . . . . . . . . . . 12
    ![]. ].](_drbrack.gif)
  ![]. ].](_drbrack.gif)      ![]. ].](_drbrack.gif)  

     ![]. ].](_drbrack.gif)     |
54 | 36, 53 | bitri 257 |
. . . . . . . . . . 11
   ![]. ].](_drbrack.gif)       ![]. ].](_drbrack.gif)  

     ![]. ].](_drbrack.gif)     |
55 | 54 | albii 1699 |
. . . . . . . . . 10
     ![]. ].](_drbrack.gif)       ![]. ].](_drbrack.gif)  
        ![]. ].](_drbrack.gif)     |
56 | 34, 55 | bitri 257 |
. . . . . . . . 9
   ![]. ].](_drbrack.gif)   
  
  ![]. ].](_drbrack.gif)         
 ![]. ].](_drbrack.gif)     |
57 | 33, 56 | bitri 257 |
. . . . . . . 8
   ![]. ].](_drbrack.gif) 
   
 ![]. ].](_drbrack.gif) 
        ![]. ].](_drbrack.gif)     |
58 | | bnj110.2 |
. . . . . . . . 9
     
 ![]. ].](_drbrack.gif)    |
59 | 58 | sbcbii 3311 |
. . . . . . . 8
   ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif) 
     ![]. ].](_drbrack.gif)    |
60 | | df-ral 2761 |
. . . . . . . 8
 
   
 ![]. ].](_drbrack.gif) 
        ![]. ].](_drbrack.gif)     |
61 | 57, 59, 60 | 3bitr4i 285 |
. . . . . . 7
   ![]. ].](_drbrack.gif)     
 ![]. ].](_drbrack.gif)    |
62 | 31, 61 | sylibr 217 |
. . . . . 6
 

  
  ![]. ].](_drbrack.gif)   |
63 | 29, 62 | bnj31 29597 |
. . . . 5
   
      ![]. ].](_drbrack.gif)   |
64 | | nfv 1769 |
. . . . . . . 8
     |
65 | | nfsbc1v 3275 |
. . . . . . . . 9
  
 ![]. ].](_drbrack.gif)  |
66 | | nfsbc1v 3275 |
. . . . . . . . 9
  
 ![]. ].](_drbrack.gif)  |
67 | 65, 66 | nfim 2023 |
. . . . . . . 8
     ![]. ].](_drbrack.gif)
  ![]. ].](_drbrack.gif)   |
68 | | sbceq1a 3266 |
. . . . . . . . 9
    ![]. ].](_drbrack.gif)    |
69 | | sbceq1a 3266 |
. . . . . . . . 9
    ![]. ].](_drbrack.gif)    |
70 | 68, 69 | imbi12d 327 |
. . . . . . . 8
       ![]. ].](_drbrack.gif)
  ![]. ].](_drbrack.gif)     |
71 | 64, 67, 70 | cbvral 3001 |
. . . . . . 7
 
 

   ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)    |
72 | | elrabi 3181 |
. . . . . . . . 9
     |
73 | 72 | imim1i 59 |
. . . . . . . 8
     ![]. ].](_drbrack.gif)
  ![]. ].](_drbrack.gif)         ![]. ].](_drbrack.gif)
  ![]. ].](_drbrack.gif)     |
74 | 73 | ralimi2 2793 |
. . . . . . 7
 
 
 ![]. ].](_drbrack.gif)
  ![]. ].](_drbrack.gif)  

    ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)    |
75 | 71, 74 | sylbi 200 |
. . . . . 6
 
      
 ![]. ].](_drbrack.gif)
  ![]. ].](_drbrack.gif)    |
76 | | rexim 2849 |
. . . . . 6
 

    ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif) 
 

    ![]. ].](_drbrack.gif)       ![]. ].](_drbrack.gif)    |
77 | 75, 76 | syl 17 |
. . . . 5
 
   

    ![]. ].](_drbrack.gif)       ![]. ].](_drbrack.gif)    |
78 | 63, 77 | mpan9 477 |
. . . 4
      
        ![]. ].](_drbrack.gif)   |
79 | 78 | an32s 821 |
. . 3
    
 

 

    ![]. ].](_drbrack.gif)   |
80 | 18, 79 | mto 181 |
. 2
   
 

  |
81 | | iman 431 |
. 2
    
 


   
 

   |
82 | 80, 81 | mpbir 214 |
1
   
     |