Step | Hyp | Ref
| Expression |
1 | | cmvrs 34127 |
. 2
class
mVars |
2 | | vt |
. . 3
setvar π‘ |
3 | | cvv 3447 |
. . 3
class
V |
4 | | ve |
. . . 4
setvar π |
5 | 2 | cv 1541 |
. . . . 5
class π‘ |
6 | | cmex 34125 |
. . . . 5
class
mEx |
7 | 5, 6 | cfv 6500 |
. . . 4
class
(mExβπ‘) |
8 | 4 | cv 1541 |
. . . . . . 7
class π |
9 | | c2nd 7924 |
. . . . . . 7
class
2nd |
10 | 8, 9 | cfv 6500 |
. . . . . 6
class
(2nd βπ) |
11 | 10 | crn 5638 |
. . . . 5
class ran
(2nd βπ) |
12 | | cmvar 34119 |
. . . . . 6
class
mVR |
13 | 5, 12 | cfv 6500 |
. . . . 5
class
(mVRβπ‘) |
14 | 11, 13 | cin 3913 |
. . . 4
class (ran
(2nd βπ)
β© (mVRβπ‘)) |
15 | 4, 7, 14 | cmpt 5192 |
. . 3
class (π β (mExβπ‘) β¦ (ran (2nd
βπ) β©
(mVRβπ‘))) |
16 | 2, 3, 15 | cmpt 5192 |
. 2
class (π‘ β V β¦ (π β (mExβπ‘) β¦ (ran (2nd
βπ) β©
(mVRβπ‘)))) |
17 | 1, 16 | wceq 1542 |
1
wff mVars =
(π‘ β V β¦ (π β (mExβπ‘) β¦ (ran (2nd
βπ) β©
(mVRβπ‘)))) |