Detailed syntax breakdown of Definition df-mvrs
Step | Hyp | Ref
| Expression |
1 | | cmvrs 33439 |
. 2
class
mVars |
2 | | vt |
. . 3
setvar 𝑡 |
3 | | cvv 3429 |
. . 3
class
V |
4 | | ve |
. . . 4
setvar 𝑒 |
5 | 2 | cv 1538 |
. . . . 5
class 𝑡 |
6 | | cmex 33437 |
. . . . 5
class
mEx |
7 | 5, 6 | cfv 6426 |
. . . 4
class
(mEx‘𝑡) |
8 | 4 | cv 1538 |
. . . . . . 7
class 𝑒 |
9 | | c2nd 7819 |
. . . . . . 7
class
2nd |
10 | 8, 9 | cfv 6426 |
. . . . . 6
class
(2nd ‘𝑒) |
11 | 10 | crn 5585 |
. . . . 5
class ran
(2nd ‘𝑒) |
12 | | cmvar 33431 |
. . . . . 6
class
mVR |
13 | 5, 12 | cfv 6426 |
. . . . 5
class
(mVR‘𝑡) |
14 | 11, 13 | cin 3885 |
. . . 4
class (ran
(2nd ‘𝑒)
∩ (mVR‘𝑡)) |
15 | 4, 7, 14 | cmpt 5156 |
. . 3
class (𝑒 ∈ (mEx‘𝑡) ↦ (ran (2nd
‘𝑒) ∩
(mVR‘𝑡))) |
16 | 2, 3, 15 | cmpt 5156 |
. 2
class (𝑡 ∈ V ↦ (𝑒 ∈ (mEx‘𝑡) ↦ (ran (2nd
‘𝑒) ∩
(mVR‘𝑡)))) |
17 | 1, 16 | wceq 1539 |
1
wff mVars =
(𝑡 ∈ V ↦ (𝑒 ∈ (mEx‘𝑡) ↦ (ran (2nd
‘𝑒) ∩
(mVR‘𝑡)))) |