Detailed syntax breakdown of Definition df-mvrs
Step | Hyp | Ref
| Expression |
1 | | cmvrs 31366 |
. 2
class
mVars |
2 | | vt |
. . 3
setvar 𝑡 |
3 | | cvv 3200 |
. . 3
class
V |
4 | | ve |
. . . 4
setvar 𝑒 |
5 | 2 | cv 1482 |
. . . . 5
class 𝑡 |
6 | | cmex 31364 |
. . . . 5
class
mEx |
7 | 5, 6 | cfv 5888 |
. . . 4
class
(mEx‘𝑡) |
8 | 4 | cv 1482 |
. . . . . . 7
class 𝑒 |
9 | | c2nd 7167 |
. . . . . . 7
class
2nd |
10 | 8, 9 | cfv 5888 |
. . . . . 6
class
(2nd ‘𝑒) |
11 | 10 | crn 5115 |
. . . . 5
class ran
(2nd ‘𝑒) |
12 | | cmvar 31358 |
. . . . . 6
class
mVR |
13 | 5, 12 | cfv 5888 |
. . . . 5
class
(mVR‘𝑡) |
14 | 11, 13 | cin 3573 |
. . . 4
class (ran
(2nd ‘𝑒)
∩ (mVR‘𝑡)) |
15 | 4, 7, 14 | cmpt 4729 |
. . 3
class (𝑒 ∈ (mEx‘𝑡) ↦ (ran (2nd
‘𝑒) ∩
(mVR‘𝑡))) |
16 | 2, 3, 15 | cmpt 4729 |
. 2
class (𝑡 ∈ V ↦ (𝑒 ∈ (mEx‘𝑡) ↦ (ran (2nd
‘𝑒) ∩
(mVR‘𝑡)))) |
17 | 1, 16 | wceq 1483 |
1
wff mVars =
(𝑡 ∈ V ↦ (𝑒 ∈ (mEx‘𝑡) ↦ (ran (2nd
‘𝑒) ∩
(mVR‘𝑡)))) |