Step | Hyp | Ref
| Expression |
1 | | idn1 36944 |
. . . . . . . . . . . . . . . . . . 19

  |
2 | | sbcel12gOLD 36905 |
. . . . . . . . . . . . . . . . . . 19
  
 ![]. ].](_drbrack.gif)
  ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)    |
3 | 1, 2 | e1a 37006 |
. . . . . . . . . . . . . . . . . 18

   ![]. ].](_drbrack.gif)   ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)    |
4 | | csbconstg 3376 |
. . . . . . . . . . . . . . . . . . . 20
   ![]_ ]_](_urbrack.gif)   |
5 | 1, 4 | e1a 37006 |
. . . . . . . . . . . . . . . . . . 19

  ![]_ ]_](_urbrack.gif)
  |
6 | | eleq1 2517 |
. . . . . . . . . . . . . . . . . . 19
   ![]_ ]_](_urbrack.gif)
   ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)    |
7 | 5, 6 | e1a 37006 |
. . . . . . . . . . . . . . . . . 18

   ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)    |
8 | | bibi1 329 |
. . . . . . . . . . . . . . . . . . 19
    ![]. ].](_drbrack.gif)
  ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)      ![]. ].](_drbrack.gif)
  ![]_ ]_](_urbrack.gif)     ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)     |
9 | 8 | biimprd 227 |
. . . . . . . . . . . . . . . . . 18
    ![]. ].](_drbrack.gif)
  ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)      ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)     ![]. ].](_drbrack.gif)
  ![]_ ]_](_urbrack.gif)     |
10 | 3, 7, 9 | e11 37067 |
. . . . . . . . . . . . . . . . 17

   ![]. ].](_drbrack.gif)
  ![]_ ]_](_urbrack.gif)    |
11 | | sbcel12gOLD 36905 |
. . . . . . . . . . . . . . . . . . 19
  
 ![]. ].](_drbrack.gif)
  ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)    |
12 | 1, 11 | e1a 37006 |
. . . . . . . . . . . . . . . . . 18

   ![]. ].](_drbrack.gif)   ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)    |
13 | | csbconstg 3376 |
. . . . . . . . . . . . . . . . . . . 20
   ![]_ ]_](_urbrack.gif)   |
14 | 1, 13 | e1a 37006 |
. . . . . . . . . . . . . . . . . . 19

  ![]_ ]_](_urbrack.gif)
  |
15 | | eleq1 2517 |
. . . . . . . . . . . . . . . . . . 19
   ![]_ ]_](_urbrack.gif)
   ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)    |
16 | 14, 15 | e1a 37006 |
. . . . . . . . . . . . . . . . . 18

   ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)    |
17 | | bibi1 329 |
. . . . . . . . . . . . . . . . . . 19
    ![]. ].](_drbrack.gif)
  ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)      ![]. ].](_drbrack.gif)   ![]_ ]_](_urbrack.gif)     ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)     |
18 | 17 | biimprd 227 |
. . . . . . . . . . . . . . . . . 18
    ![]. ].](_drbrack.gif)
  ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)      ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif) 
   ![]. ].](_drbrack.gif)
  ![]_ ]_](_urbrack.gif)     |
19 | 12, 16, 18 | e11 37067 |
. . . . . . . . . . . . . . . . 17

   ![]. ].](_drbrack.gif)   ![]_ ]_](_urbrack.gif)    |
20 | | pm4.38 883 |
. . . . . . . . . . . . . . . . . 18
     ![]. ].](_drbrack.gif)   ![]_ ]_](_urbrack.gif)     ![]. ].](_drbrack.gif)
  ![]_ ]_](_urbrack.gif)       ![]. ].](_drbrack.gif)
  ![]. ].](_drbrack.gif) 
   ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)     |
21 | 20 | ex 436 |
. . . . . . . . . . . . . . . . 17
    ![]. ].](_drbrack.gif)
  ![]_ ]_](_urbrack.gif)      ![]. ].](_drbrack.gif)   ![]_ ]_](_urbrack.gif) 
  
 ![]. ].](_drbrack.gif)
  ![]. ].](_drbrack.gif)
    ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)      |
22 | 10, 19, 21 | e11 37067 |
. . . . . . . . . . . . . . . 16

    ![]. ].](_drbrack.gif)
  ![]. ].](_drbrack.gif) 
   ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)     |
23 | | sbcangOLD 36890 |
. . . . . . . . . . . . . . . . 17
  
 ![]. ].](_drbrack.gif) 
    ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)     |
24 | 1, 23 | e1a 37006 |
. . . . . . . . . . . . . . . 16

   ![]. ].](_drbrack.gif)  
   ![]. ].](_drbrack.gif)
  ![]. ].](_drbrack.gif)     |
25 | | bibi1 329 |
. . . . . . . . . . . . . . . . 17
    ![]. ].](_drbrack.gif) 
    ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)       ![]. ].](_drbrack.gif)  
   ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)  
  
 ![]. ].](_drbrack.gif)
  ![]. ].](_drbrack.gif)
    ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)      |
26 | 25 | biimprcd 229 |
. . . . . . . . . . . . . . . 16
     ![]. ].](_drbrack.gif)   ![]. ].](_drbrack.gif)
    ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)       ![]. ].](_drbrack.gif)  
   ![]. ].](_drbrack.gif)
  ![]. ].](_drbrack.gif)      ![]. ].](_drbrack.gif) 
    ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)      |
27 | 22, 24, 26 | e11 37067 |
. . . . . . . . . . . . . . 15

   ![]. ].](_drbrack.gif)  
   ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)     |
28 | | sbcg 3333 |
. . . . . . . . . . . . . . . 16
  
 ![]. ].](_drbrack.gif)
  
      |
29 | 1, 28 | e1a 37006 |
. . . . . . . . . . . . . . 15

   ![]. ].](_drbrack.gif)          |
30 | | pm4.38 883 |
. . . . . . . . . . . . . . . 16
     ![]. ].](_drbrack.gif)   
   
   ![]. ].](_drbrack.gif) 
    ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)   
  
 ![]. ].](_drbrack.gif)
     ![]. ].](_drbrack.gif)   
       ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)      |
31 | 30 | expcom 437 |
. . . . . . . . . . . . . . 15
    ![]. ].](_drbrack.gif) 
    ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)       ![]. ].](_drbrack.gif)       
    ![]. ].](_drbrack.gif)
     ![]. ].](_drbrack.gif)   
       ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)       |
32 | 27, 29, 31 | e11 37067 |
. . . . . . . . . . . . . 14

    ![]. ].](_drbrack.gif)      ![]. ].](_drbrack.gif)   
       ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)      |
33 | | sbcangOLD 36890 |
. . . . . . . . . . . . . . 15
  
 ![]. ].](_drbrack.gif)     
     ![]. ].](_drbrack.gif)      ![]. ].](_drbrack.gif) 
     |
34 | 1, 33 | e1a 37006 |
. . . . . . . . . . . . . 14

   ![]. ].](_drbrack.gif)       
   ![]. ].](_drbrack.gif)      ![]. ].](_drbrack.gif)       |
35 | | bibi1 329 |
. . . . . . . . . . . . . . 15
    ![]. ].](_drbrack.gif)     
     ![]. ].](_drbrack.gif)      ![]. ].](_drbrack.gif) 
       ![]. ].](_drbrack.gif)       
       ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)        ![]. ].](_drbrack.gif)      ![]. ].](_drbrack.gif) 
 
       ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)       |
36 | 35 | biimprcd 229 |
. . . . . . . . . . . . . 14
     ![]. ].](_drbrack.gif)      ![]. ].](_drbrack.gif)   
       ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)        ![]. ].](_drbrack.gif)     
     ![]. ].](_drbrack.gif)      ![]. ].](_drbrack.gif) 
      ![]. ].](_drbrack.gif)     
         ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)       |
37 | 32, 34, 36 | e11 37067 |
. . . . . . . . . . . . 13

   ![]. ].](_drbrack.gif)       
       ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)      |
38 | 37 | gen11 36995 |
. . . . . . . . . . . 12

     ![]. ].](_drbrack.gif)     
         ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)      |
39 | | exbi 1716 |
. . . . . . . . . . . 12
      ![]. ].](_drbrack.gif)       
       ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)       
 ![]. ].](_drbrack.gif)     
           ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)      |
40 | 38, 39 | e1a 37006 |
. . . . . . . . . . 11

   
 ![]. ].](_drbrack.gif)     
           ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)      |
41 | | sbcexgOLD 36904 |
. . . . . . . . . . . 12
  
 ![]. ].](_drbrack.gif)         
  
 ![]. ].](_drbrack.gif)     
     |
42 | 1, 41 | e1a 37006 |
. . . . . . . . . . 11

   ![]. ].](_drbrack.gif)       
      ![]. ].](_drbrack.gif)           |
43 | | bibi1 329 |
. . . . . . . . . . . 12
    ![]. ].](_drbrack.gif)         
  
 ![]. ].](_drbrack.gif)     
       ![]. ].](_drbrack.gif)         
         ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)       
 ![]. ].](_drbrack.gif)     
           ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)       |
44 | 43 | biimprcd 229 |
. . . . . . . . . . 11
      ![]. ].](_drbrack.gif)       
         ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)   
  
 ![]. ].](_drbrack.gif)         
  
 ![]. ].](_drbrack.gif)     
    
 ![]. ].](_drbrack.gif)         
         ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)       |
45 | 40, 42, 44 | e11 37067 |
. . . . . . . . . 10

   ![]. ].](_drbrack.gif)       
           ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)      |
46 | 45 | gen11 36995 |
. . . . . . . . 9

     ![]. ].](_drbrack.gif)       
 
         ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)      |
47 | | exbi 1716 |
. . . . . . . . 9
      ![]. ].](_drbrack.gif)       
           ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)       
 ![]. ].](_drbrack.gif)         
           ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)      |
48 | 46, 47 | e1a 37006 |
. . . . . . . 8

   
 ![]. ].](_drbrack.gif)         
           ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)      |
49 | | sbcexgOLD 36904 |
. . . . . . . . 9
  
 ![]. ].](_drbrack.gif)         
      ![]. ].](_drbrack.gif)       
     |
50 | 1, 49 | e1a 37006 |
. . . . . . . 8

   ![]. ].](_drbrack.gif)         
 
  
 ![]. ].](_drbrack.gif)             |
51 | | bibi1 329 |
. . . . . . . . 9
    ![]. ].](_drbrack.gif)         
      ![]. ].](_drbrack.gif)       
       ![]. ].](_drbrack.gif)         
             ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)       
 ![]. ].](_drbrack.gif)         
           ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)       |
52 | 51 | biimprcd 229 |
. . . . . . . 8
      ![]. ].](_drbrack.gif)       
             ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)   
  
 ![]. ].](_drbrack.gif)         
      ![]. ].](_drbrack.gif)       
    
 ![]. ].](_drbrack.gif)         
             ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)       |
53 | 48, 50, 52 | e11 37067 |
. . . . . . 7

   ![]. ].](_drbrack.gif)         
 
           ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)      |
54 | 53 | gen11 36995 |
. . . . . 6

     ![]. ].](_drbrack.gif)           
           ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)      |
55 | | abbi 2565 |
. . . . . . 7
      ![]. ].](_drbrack.gif)         
 
           ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)   
   ![]. ].](_drbrack.gif)         
               ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)      |
56 | 55 | biimpi 198 |
. . . . . 6
      ![]. ].](_drbrack.gif)         
 
           ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)       ![]. ].](_drbrack.gif)         
               ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)      |
57 | 54, 56 | e1a 37006 |
. . . . 5

   ![]. ].](_drbrack.gif)         
               ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)      |
58 | | csbabgOLD 37211 |
. . . . . 6
   ![]_ ]_](_urbrack.gif)          
      ![]. ].](_drbrack.gif)               |
59 | 1, 58 | e1a 37006 |
. . . . 5

  ![]_ ]_](_urbrack.gif)                 ![]. ].](_drbrack.gif)         
     |
60 | | eqeq2 2462 |
. . . . . 6
    ![]. ].](_drbrack.gif)         
               ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)          
      ![]. ].](_drbrack.gif)             
 ![]_ ]_](_urbrack.gif)                          ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)       |
61 | 60 | biimpd 211 |
. . . . 5
    ![]. ].](_drbrack.gif)         
               ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)          
      ![]. ].](_drbrack.gif)               ![]_ ]_](_urbrack.gif)                          ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)       |
62 | 57, 59, 61 | e11 37067 |
. . . 4

  ![]_ ]_](_urbrack.gif)                          ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)      |
63 | | df-xp 4840 |
. . . . . . 7
     

   |
64 | | df-opab 4462 |
. . . . . . 7
    
 
         
    |
65 | 63, 64 | eqtri 2473 |
. . . . . 6
                |
66 | 65 | ax-gen 1669 |
. . . . 5
             
    |
67 | | csbeq2gOLD 36916 |
. . . . 5
               
     ![]_ ]_](_urbrack.gif) 
   ![]_ ]_](_urbrack.gif)          
      |
68 | 1, 66, 67 | e10 37073 |
. . . 4

  ![]_ ]_](_urbrack.gif)     ![]_ ]_](_urbrack.gif)          
     |
69 | | eqeq2 2462 |
. . . . 5
   ![]_ ]_](_urbrack.gif)          
               ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)     ![]_ ]_](_urbrack.gif)              
 ![]_ ]_](_urbrack.gif)               ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)       |
70 | 69 | biimpd 211 |
. . . 4
   ![]_ ]_](_urbrack.gif)          
               ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)     ![]_ ]_](_urbrack.gif)                ![]_ ]_](_urbrack.gif)               ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)       |
71 | 62, 68, 70 | e11 37067 |
. . 3

  ![]_ ]_](_urbrack.gif)               ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)      |
72 | | df-xp 4840 |
. . . 4
   ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)         ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)    |
73 | | df-opab 4462 |
. . . 4
       ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)               ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)     |
74 | 72, 73 | eqtri 2473 |
. . 3
   ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)              ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)     |
75 | | eqeq2 2462 |
. . . 4
    ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)              ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)   
   ![]_ ]_](_urbrack.gif)      ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)    ![]_ ]_](_urbrack.gif)               ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)       |
76 | 75 | biimprcd 229 |
. . 3
   ![]_ ]_](_urbrack.gif)               ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)        ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)              ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)      ![]_ ]_](_urbrack.gif)      ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)     |
77 | 71, 74, 76 | e10 37073 |
. 2

  ![]_ ]_](_urbrack.gif)      ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)    |
78 | 77 | in1 36941 |
1
   ![]_ ]_](_urbrack.gif)      ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)    |