Detailed syntax breakdown of Definition df-evl
Step | Hyp | Ref
| Expression |
1 | | cevl 21288 |
. 2
class
eval |
2 | | vi |
. . 3
setvar 𝑖 |
3 | | vr |
. . 3
setvar 𝑟 |
4 | | cvv 3431 |
. . 3
class
V |
5 | 3 | cv 1537 |
. . . . 5
class 𝑟 |
6 | | cbs 16919 |
. . . . 5
class
Base |
7 | 5, 6 | cfv 6435 |
. . . 4
class
(Base‘𝑟) |
8 | 2 | cv 1537 |
. . . . 5
class 𝑖 |
9 | | ces 21287 |
. . . . 5
class
evalSub |
10 | 8, 5, 9 | co 7282 |
. . . 4
class (𝑖 evalSub 𝑟) |
11 | 7, 10 | cfv 6435 |
. . 3
class ((𝑖 evalSub 𝑟)‘(Base‘𝑟)) |
12 | 2, 3, 4, 4, 11 | cmpo 7284 |
. 2
class (𝑖 ∈ V, 𝑟 ∈ V ↦ ((𝑖 evalSub 𝑟)‘(Base‘𝑟))) |
13 | 1, 12 | wceq 1538 |
1
wff eval =
(𝑖 ∈ V, 𝑟 ∈ V ↦ ((𝑖 evalSub 𝑟)‘(Base‘𝑟))) |