Detailed syntax breakdown of Definition df-mrsub
Step | Hyp | Ref
| Expression |
1 | | cmrsub 31367 |
. 2
mRSubst |
2 | | vt |
. . 3
|
3 | | cvv 3200 |
. . 3
|
4 | | vf |
. . . 4
|
5 | 2 | cv 1482 |
. . . . . 6
|
6 | | cmrex 31363 |
. . . . . 6
mREx |
7 | 5, 6 | cfv 5888 |
. . . . 5
mREx |
8 | | cmvar 31358 |
. . . . . 6
mVR |
9 | 5, 8 | cfv 5888 |
. . . . 5
mVR |
10 | | cpm 7858 |
. . . . 5
|
11 | 7, 9, 10 | co 6650 |
. . . 4
mREx mVR |
12 | | ve |
. . . . 5
|
13 | | cmcn 31357 |
. . . . . . . . 9
mCN |
14 | 5, 13 | cfv 5888 |
. . . . . . . 8
mCN |
15 | 14, 9 | cun 3572 |
. . . . . . 7
mCN mVR |
16 | | cfrmd 17384 |
. . . . . . 7
freeMnd |
17 | 15, 16 | cfv 5888 |
. . . . . 6
freeMndmCN mVR |
18 | | vv |
. . . . . . . 8
|
19 | 18 | cv 1482 |
. . . . . . . . . 10
|
20 | 4 | cv 1482 |
. . . . . . . . . . 11
|
21 | 20 | cdm 5114 |
. . . . . . . . . 10
|
22 | 19, 21 | wcel 1990 |
. . . . . . . . 9
|
23 | 19, 20 | cfv 5888 |
. . . . . . . . 9
|
24 | 19 | cs1 13294 |
. . . . . . . . 9
|
25 | 22, 23, 24 | cif 4086 |
. . . . . . . 8
|
26 | 18, 15, 25 | cmpt 4729 |
. . . . . . 7
mCN mVR
|
27 | 12 | cv 1482 |
. . . . . . 7
|
28 | 26, 27 | ccom 5118 |
. . . . . 6
mCN mVR |
29 | | cgsu 16101 |
. . . . . 6
g |
30 | 17, 28, 29 | co 6650 |
. . . . 5
freeMndmCN mVR g mCN mVR
|
31 | 12, 7, 30 | cmpt 4729 |
. . . 4
mREx freeMndmCN mVR g mCN mVR
|
32 | 4, 11, 31 | cmpt 4729 |
. . 3
mREx mVR mREx freeMndmCN mVR g mCN mVR
|
33 | 2, 3, 32 | cmpt 4729 |
. 2
mREx mVR mREx freeMndmCN mVR g mCN mVR
|
34 | 1, 33 | wceq 1483 |
1
mRSubst mREx mVR mREx freeMndmCN mVR g mCN mVR
|