Detailed syntax breakdown of Definition df-add
Step | Hyp | Ref
| Expression |
1 | | caddc 7813 |
. 2
 |
2 | | vx |
. . . . . . 7
 |
3 | 2 | cv 1352 |
. . . . . 6
 |
4 | | cc 7808 |
. . . . . 6
 |
5 | 3, 4 | wcel 2148 |
. . . . 5
 |
6 | | vy |
. . . . . . 7
 |
7 | 6 | cv 1352 |
. . . . . 6
 |
8 | 7, 4 | wcel 2148 |
. . . . 5
 |
9 | 5, 8 | wa 104 |
. . . 4
   |
10 | | vw |
. . . . . . . . . . . . 13
 |
11 | 10 | cv 1352 |
. . . . . . . . . . . 12
 |
12 | | vv |
. . . . . . . . . . . . 13
 |
13 | 12 | cv 1352 |
. . . . . . . . . . . 12
 |
14 | 11, 13 | cop 3595 |
. . . . . . . . . . 11
    |
15 | 3, 14 | wceq 1353 |
. . . . . . . . . 10
    |
16 | | vu |
. . . . . . . . . . . . 13
 |
17 | 16 | cv 1352 |
. . . . . . . . . . . 12
 |
18 | | vf |
. . . . . . . . . . . . 13
 |
19 | 18 | cv 1352 |
. . . . . . . . . . . 12
 |
20 | 17, 19 | cop 3595 |
. . . . . . . . . . 11
    |
21 | 7, 20 | wceq 1353 |
. . . . . . . . . 10
    |
22 | 15, 21 | wa 104 |
. . . . . . . . 9
         |
23 | | vz |
. . . . . . . . . . 11
 |
24 | 23 | cv 1352 |
. . . . . . . . . 10
 |
25 | | cplr 7299 |
. . . . . . . . . . . 12
 |
26 | 11, 17, 25 | co 5874 |
. . . . . . . . . . 11
   |
27 | 13, 19, 25 | co 5874 |
. . . . . . . . . . 11
   |
28 | 26, 27 | cop 3595 |
. . . . . . . . . 10
        |
29 | 24, 28 | wceq 1353 |
. . . . . . . . 9
        |
30 | 22, 29 | wa 104 |
. . . . . . . 8
        
         |
31 | 30, 18 | wex 1492 |
. . . . . . 7
      
   
         |
32 | 31, 16 | wex 1492 |
. . . . . 6
            
         |
33 | 32, 12 | wex 1492 |
. . . . 5
              
         |
34 | 33, 10 | wex 1492 |
. . . 4
                
         |
35 | 9, 34 | wa 104 |
. . 3
 
                 
          |
36 | 35, 2, 6, 23 | coprab 5875 |
. 2
                      
   
           |
37 | 1, 36 | wceq 1353 |
1
     
                    
           |