Detailed syntax breakdown of Definition df-evl
Step | Hyp | Ref
| Expression |
1 | | cevl 19505 |
. 2
class
eval |
2 | | vi |
. . 3
setvar 𝑖 |
3 | | vr |
. . 3
setvar 𝑟 |
4 | | cvv 3200 |
. . 3
class
V |
5 | 3 | cv 1482 |
. . . . 5
class 𝑟 |
6 | | cbs 15857 |
. . . . 5
class
Base |
7 | 5, 6 | cfv 5888 |
. . . 4
class
(Base‘𝑟) |
8 | 2 | cv 1482 |
. . . . 5
class 𝑖 |
9 | | ces 19504 |
. . . . 5
class
evalSub |
10 | 8, 5, 9 | co 6650 |
. . . 4
class (𝑖 evalSub 𝑟) |
11 | 7, 10 | cfv 5888 |
. . 3
class ((𝑖 evalSub 𝑟)‘(Base‘𝑟)) |
12 | 2, 3, 4, 4, 11 | cmpt2 6652 |
. 2
class (𝑖 ∈ V, 𝑟 ∈ V ↦ ((𝑖 evalSub 𝑟)‘(Base‘𝑟))) |
13 | 1, 12 | wceq 1483 |
1
wff eval =
(𝑖 ∈ V, 𝑟 ∈ V ↦ ((𝑖 evalSub 𝑟)‘(Base‘𝑟))) |