Detailed syntax breakdown of Definition df-mrsub
Step | Hyp | Ref
| Expression |
1 | | cmrsub 30108 |
. 2
mRSubst |
2 | | vt |
. . 3
 |
3 | | cvv 3045 |
. . 3
 |
4 | | vf |
. . . 4
 |
5 | 2 | cv 1443 |
. . . . . 6
 |
6 | | cmrex 30104 |
. . . . . 6
mREx |
7 | 5, 6 | cfv 5582 |
. . . . 5
mREx   |
8 | | cmvar 30099 |
. . . . . 6
mVR |
9 | 5, 8 | cfv 5582 |
. . . . 5
mVR   |
10 | | cpm 7473 |
. . . . 5
 |
11 | 7, 9, 10 | co 6290 |
. . . 4
 mREx  mVR    |
12 | | ve |
. . . . 5
 |
13 | | cmcn 30098 |
. . . . . . . . 9
mCN |
14 | 5, 13 | cfv 5582 |
. . . . . . . 8
mCN   |
15 | 14, 9 | cun 3402 |
. . . . . . 7
 mCN  mVR    |
16 | | cfrmd 16631 |
. . . . . . 7
freeMnd |
17 | 15, 16 | cfv 5582 |
. . . . . 6
freeMnd  mCN  mVR     |
18 | | vv |
. . . . . . . 8
 |
19 | 18 | cv 1443 |
. . . . . . . . . 10
 |
20 | 4 | cv 1443 |
. . . . . . . . . . 11
 |
21 | 20 | cdm 4834 |
. . . . . . . . . 10
 |
22 | 19, 21 | wcel 1887 |
. . . . . . . . 9
 |
23 | 19, 20 | cfv 5582 |
. . . . . . . . 9
     |
24 | 19 | cs1 12659 |
. . . . . . . . 9
     |
25 | 22, 23, 24 | cif 3881 |
. . . . . . . 8
              |
26 | 18, 15, 25 | cmpt 4461 |
. . . . . . 7
  mCN  mVR     
            |
27 | 12 | cv 1443 |
. . . . . . 7
 |
28 | 26, 27 | ccom 4838 |
. . . . . 6
   mCN  mVR                   |
29 | | cgsu 15339 |
. . . . . 6
g |
30 | 17, 28, 29 | co 6290 |
. . . . 5
 freeMnd  mCN  mVR    g    mCN  mVR     
              |
31 | 12, 7, 30 | cmpt 4461 |
. . . 4
 mREx   freeMnd  mCN  mVR    g    mCN  mVR     
               |
32 | 4, 11, 31 | cmpt 4461 |
. . 3
  mREx  mVR    mREx   freeMnd  mCN  mVR    g    mCN  mVR     
                |
33 | 2, 3, 32 | cmpt 4461 |
. 2
   mREx  mVR    mREx   freeMnd  mCN  mVR    g    mCN  mVR     
                 |
34 | 1, 33 | wceq 1444 |
1
mRSubst    mREx  mVR    mREx   freeMnd  mCN  mVR    g    mCN  mVR     
                 |