Detailed syntax breakdown of Definition df-shft
Step | Hyp | Ref
| Expression |
1 | | cshi 10718 |
. 2
class
shift |
2 | | vf |
. . 3
setvar 𝑓 |
3 | | vx |
. . 3
setvar 𝑥 |
4 | | cvv 2712 |
. . 3
class
V |
5 | | cc 7731 |
. . 3
class
ℂ |
6 | | vy |
. . . . . . 7
setvar 𝑦 |
7 | 6 | cv 1334 |
. . . . . 6
class 𝑦 |
8 | 7, 5 | wcel 2128 |
. . . . 5
wff 𝑦 ∈ ℂ |
9 | 3 | cv 1334 |
. . . . . . 7
class 𝑥 |
10 | | cmin 8047 |
. . . . . . 7
class
− |
11 | 7, 9, 10 | co 5825 |
. . . . . 6
class (𝑦 − 𝑥) |
12 | | vz |
. . . . . . 7
setvar 𝑧 |
13 | 12 | cv 1334 |
. . . . . 6
class 𝑧 |
14 | 2 | cv 1334 |
. . . . . 6
class 𝑓 |
15 | 11, 13, 14 | wbr 3966 |
. . . . 5
wff (𝑦 − 𝑥)𝑓𝑧 |
16 | 8, 15 | wa 103 |
. . . 4
wff (𝑦 ∈ ℂ ∧ (𝑦 − 𝑥)𝑓𝑧) |
17 | 16, 6, 12 | copab 4025 |
. . 3
class
{〈𝑦, 𝑧〉 ∣ (𝑦 ∈ ℂ ∧ (𝑦 − 𝑥)𝑓𝑧)} |
18 | 2, 3, 4, 5, 17 | cmpo 5827 |
. 2
class (𝑓 ∈ V, 𝑥 ∈ ℂ ↦ {〈𝑦, 𝑧〉 ∣ (𝑦 ∈ ℂ ∧ (𝑦 − 𝑥)𝑓𝑧)}) |
19 | 1, 18 | wceq 1335 |
1
wff shift =
(𝑓 ∈ V, 𝑥 ∈ ℂ ↦
{〈𝑦, 𝑧〉 ∣ (𝑦 ∈ ℂ ∧ (𝑦 − 𝑥)𝑓𝑧)}) |