Detailed syntax breakdown of Definition df-shft
Step | Hyp | Ref
| Expression |
1 | | cshi 9702 |
. 2
class
shift |
2 | | vf |
. . 3
setvar 𝑓 |
3 | | vx |
. . 3
setvar 𝑥 |
4 | | cvv 2601 |
. . 3
class
V |
5 | | cc 6979 |
. . 3
class
ℂ |
6 | | vy |
. . . . . . 7
setvar 𝑦 |
7 | 6 | cv 1283 |
. . . . . 6
class 𝑦 |
8 | 7, 5 | wcel 1433 |
. . . . 5
wff 𝑦 ∈ ℂ |
9 | 3 | cv 1283 |
. . . . . . 7
class 𝑥 |
10 | | cmin 7279 |
. . . . . . 7
class
− |
11 | 7, 9, 10 | co 5532 |
. . . . . 6
class (𝑦 − 𝑥) |
12 | | vz |
. . . . . . 7
setvar 𝑧 |
13 | 12 | cv 1283 |
. . . . . 6
class 𝑧 |
14 | 2 | cv 1283 |
. . . . . 6
class 𝑓 |
15 | 11, 13, 14 | wbr 3785 |
. . . . 5
wff (𝑦 − 𝑥)𝑓𝑧 |
16 | 8, 15 | wa 102 |
. . . 4
wff (𝑦 ∈ ℂ ∧ (𝑦 − 𝑥)𝑓𝑧) |
17 | 16, 6, 12 | copab 3838 |
. . 3
class
{〈𝑦, 𝑧〉 ∣ (𝑦 ∈ ℂ ∧ (𝑦 − 𝑥)𝑓𝑧)} |
18 | 2, 3, 4, 5, 17 | cmpt2 5534 |
. 2
class (𝑓 ∈ V, 𝑥 ∈ ℂ ↦ {〈𝑦, 𝑧〉 ∣ (𝑦 ∈ ℂ ∧ (𝑦 − 𝑥)𝑓𝑧)}) |
19 | 1, 18 | wceq 1284 |
1
wff shift =
(𝑓 ∈ V, 𝑥 ∈ ℂ ↦
{〈𝑦, 𝑧〉 ∣ (𝑦 ∈ ℂ ∧ (𝑦 − 𝑥)𝑓𝑧)}) |