Detailed syntax breakdown of Definition df-cid
Step | Hyp | Ref
| Expression |
1 | | ccid 15649 |
. 2
 |
2 | | vc |
. . 3
 |
3 | | ccat 15648 |
. . 3
 |
4 | | vb |
. . . 4
 |
5 | 2 | cv 1451 |
. . . . 5
 |
6 | | cbs 15199 |
. . . . 5
 |
7 | 5, 6 | cfv 5589 |
. . . 4
     |
8 | | vh |
. . . . 5
 |
9 | | chom 15279 |
. . . . . 6
 |
10 | 5, 9 | cfv 5589 |
. . . . 5
    |
11 | | vo |
. . . . . 6
 |
12 | | cco 15280 |
. . . . . . 7
comp |
13 | 5, 12 | cfv 5589 |
. . . . . 6
comp   |
14 | | vx |
. . . . . . 7
 |
15 | 4 | cv 1451 |
. . . . . . 7
 |
16 | | vg |
. . . . . . . . . . . . . 14
 |
17 | 16 | cv 1451 |
. . . . . . . . . . . . 13
 |
18 | | vf |
. . . . . . . . . . . . . 14
 |
19 | 18 | cv 1451 |
. . . . . . . . . . . . 13
 |
20 | | vy |
. . . . . . . . . . . . . . . 16
 |
21 | 20 | cv 1451 |
. . . . . . . . . . . . . . 15
 |
22 | 14 | cv 1451 |
. . . . . . . . . . . . . . 15
 |
23 | 21, 22 | cop 3965 |
. . . . . . . . . . . . . 14
    |
24 | 11 | cv 1451 |
. . . . . . . . . . . . . 14
 |
25 | 23, 22, 24 | co 6308 |
. . . . . . . . . . . . 13
        |
26 | 17, 19, 25 | co 6308 |
. . . . . . . . . . . 12
            |
27 | 26, 19 | wceq 1452 |
. . . . . . . . . . 11
            |
28 | 8 | cv 1451 |
. . . . . . . . . . . 12
 |
29 | 21, 22, 28 | co 6308 |
. . . . . . . . . . 11
     |
30 | 27, 18, 29 | wral 2756 |
. . . . . . . . . 10
                  |
31 | 22, 22 | cop 3965 |
. . . . . . . . . . . . . 14
    |
32 | 31, 21, 24 | co 6308 |
. . . . . . . . . . . . 13
        |
33 | 19, 17, 32 | co 6308 |
. . . . . . . . . . . 12
            |
34 | 33, 19 | wceq 1452 |
. . . . . . . . . . 11
            |
35 | 22, 21, 28 | co 6308 |
. . . . . . . . . . 11
     |
36 | 34, 18, 35 | wral 2756 |
. . . . . . . . . 10
                  |
37 | 30, 36 | wa 376 |
. . . . . . . . 9
 
                                   |
38 | 37, 20, 15 | wral 2756 |
. . . . . . . 8

 
                                   |
39 | 22, 22, 28 | co 6308 |
. . . . . . . 8
     |
40 | 38, 16, 39 | crio 6269 |
. . . . . . 7
       
 
                                    |
41 | 14, 15, 40 | cmpt 4454 |
. . . . . 6
        
 
                                     |
42 | 11, 13, 41 | csb 3349 |
. . . . 5
 comp   ![]_ ]_](_urbrack.gif)                            
                    |
43 | 8, 10, 42 | csb 3349 |
. . . 4
     ![]_ ]_](_urbrack.gif)  comp   ![]_ ]_](_urbrack.gif)                            
                    |
44 | 4, 7, 43 | csb 3349 |
. . 3
      ![]_ ]_](_urbrack.gif)      ![]_ ]_](_urbrack.gif)  comp   ![]_ ]_](_urbrack.gif) 
                          
                    |
45 | 2, 3, 44 | cmpt 4454 |
. 2
       ![]_ ]_](_urbrack.gif)      ![]_ ]_](_urbrack.gif)  comp   ![]_ ]_](_urbrack.gif) 
                          
                     |
46 | 1, 45 | wceq 1452 |
1
       ![]_ ]_](_urbrack.gif)      ![]_ ]_](_urbrack.gif)  comp   ![]_ ]_](_urbrack.gif)   
                        
                     |