Detailed syntax breakdown of Definition df-subr
Step | Hyp | Ref
| Expression |
1 | | cminusr 42058 |
. 2
class
-𝑟 |
2 | | vx |
. . 3
setvar 𝑥 |
3 | | vy |
. . 3
setvar 𝑦 |
4 | | cvv 3431 |
. . 3
class
V |
5 | | vv |
. . . 4
setvar 𝑣 |
6 | | cr 10881 |
. . . 4
class
ℝ |
7 | 5 | cv 1541 |
. . . . . 6
class 𝑣 |
8 | 2 | cv 1541 |
. . . . . 6
class 𝑥 |
9 | 7, 8 | cfv 6432 |
. . . . 5
class (𝑥‘𝑣) |
10 | 3 | cv 1541 |
. . . . . 6
class 𝑦 |
11 | 7, 10 | cfv 6432 |
. . . . 5
class (𝑦‘𝑣) |
12 | | cmin 11216 |
. . . . 5
class
− |
13 | 9, 11, 12 | co 7272 |
. . . 4
class ((𝑥‘𝑣) − (𝑦‘𝑣)) |
14 | 5, 6, 13 | cmpt 5162 |
. . 3
class (𝑣 ∈ ℝ ↦ ((𝑥‘𝑣) − (𝑦‘𝑣))) |
15 | 2, 3, 4, 4, 14 | cmpo 7274 |
. 2
class (𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑣 ∈ ℝ ↦ ((𝑥‘𝑣) − (𝑦‘𝑣)))) |
16 | 1, 15 | wceq 1542 |
1
wff
-𝑟 = (𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑣 ∈ ℝ ↦ ((𝑥‘𝑣) − (𝑦‘𝑣)))) |