Detailed syntax breakdown of Definition df-efg
Step | Hyp | Ref
| Expression |
1 | | cefg 17368 |
. 2
~FG |
2 | | vi |
. . 3
 |
3 | | cvv 3047 |
. . 3
 |
4 | 2 | cv 1445 |
. . . . . . . . 9
 |
5 | | c2o 7181 |
. . . . . . . . 9
 |
6 | 4, 5 | cxp 4835 |
. . . . . . . 8
   |
7 | 6 | cword 12663 |
. . . . . . 7
Word    |
8 | | vr |
. . . . . . . 8
 |
9 | 8 | cv 1445 |
. . . . . . 7
 |
10 | 7, 9 | wer 7365 |
. . . . . 6
Word    |
11 | | vx |
. . . . . . . . . . . 12
 |
12 | 11 | cv 1445 |
. . . . . . . . . . 11
 |
13 | | vn |
. . . . . . . . . . . . . 14
 |
14 | 13 | cv 1445 |
. . . . . . . . . . . . 13
 |
15 | | vy |
. . . . . . . . . . . . . . . 16
 |
16 | 15 | cv 1445 |
. . . . . . . . . . . . . . 15
 |
17 | | vz |
. . . . . . . . . . . . . . . 16
 |
18 | 17 | cv 1445 |
. . . . . . . . . . . . . . 15
 |
19 | 16, 18 | cop 3976 |
. . . . . . . . . . . . . 14
    |
20 | | c1o 7180 |
. . . . . . . . . . . . . . . 16
 |
21 | 20, 18 | cdif 3403 |
. . . . . . . . . . . . . . 15
   |
22 | 16, 21 | cop 3976 |
. . . . . . . . . . . . . 14
      |
23 | 19, 22 | cs2 12944 |
. . . . . . . . . . . . 13
              |
24 | 14, 14, 23 | cotp 3978 |
. . . . . . . . . . . 12
                  |
25 | | csplice 12668 |
. . . . . . . . . . . 12
splice |
26 | 12, 24, 25 | co 6295 |
. . . . . . . . . . 11
 splice                    |
27 | 12, 26, 9 | wbr 4405 |
. . . . . . . . . 10
   splice                    |
28 | 27, 17, 5 | wral 2739 |
. . . . . . . . 9
    splice                    |
29 | 28, 15, 4 | wral 2739 |
. . . . . . . 8

    splice                    |
30 | | cc0 9544 |
. . . . . . . . 9
 |
31 | | chash 12522 |
. . . . . . . . . 10
 |
32 | 12, 31 | cfv 5585 |
. . . . . . . . 9
     |
33 | | cfz 11791 |
. . . . . . . . 9
 |
34 | 30, 32, 33 | co 6295 |
. . . . . . . 8
         |
35 | 29, 13, 34 | wral 2739 |
. . . . . . 7
               splice                    |
36 | 35, 11, 7 | wral 2739 |
. . . . . 6
 Word              

   splice                    |
37 | 10, 36 | wa 371 |
. . . . 5
 Word   
Word                   splice                     |
38 | 37, 8 | cab 2439 |
. . . 4
  Word    Word              

   splice                      |
39 | 38 | cint 4237 |
. . 3
   Word    Word              

   splice                      |
40 | 2, 3, 39 | cmpt 4464 |
. 2
    Word    Word              

   splice                       |
41 | 1, 40 | wceq 1446 |
1
~FG
    Word    Word              

   splice                       |