MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-shft Structured version   Visualization version   GIF version

Definition df-shft 13597
Description: Define a function shifter. This operation offsets the value argument of a function (ordinarily on a subset of ) and produces a new function on . See shftval 13604 for its value. (Contributed by NM, 20-Jul-2005.)
Assertion
Ref Expression
df-shft shift = (𝑓 ∈ V, 𝑥 ∈ ℂ ↦ {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ ℂ ∧ (𝑦𝑥)𝑓𝑧)})
Distinct variable group:   𝑥,𝑦,𝑧,𝑓

Detailed syntax breakdown of Definition df-shft
StepHypRef Expression
1 cshi 13596 . 2 class shift
2 vf . . 3 setvar 𝑓
3 vx . . 3 setvar 𝑥
4 cvv 3168 . . 3 class V
5 cc 9786 . . 3 class
6 vy . . . . . . 7 setvar 𝑦
76cv 1473 . . . . . 6 class 𝑦
87, 5wcel 1975 . . . . 5 wff 𝑦 ∈ ℂ
93cv 1473 . . . . . . 7 class 𝑥
10 cmin 10113 . . . . . . 7 class
117, 9, 10co 6523 . . . . . 6 class (𝑦𝑥)
12 vz . . . . . . 7 setvar 𝑧
1312cv 1473 . . . . . 6 class 𝑧
142cv 1473 . . . . . 6 class 𝑓
1511, 13, 14wbr 4573 . . . . 5 wff (𝑦𝑥)𝑓𝑧
168, 15wa 382 . . . 4 wff (𝑦 ∈ ℂ ∧ (𝑦𝑥)𝑓𝑧)
1716, 6, 12copab 4632 . . 3 class {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ ℂ ∧ (𝑦𝑥)𝑓𝑧)}
182, 3, 4, 5, 17cmpt2 6525 . 2 class (𝑓 ∈ V, 𝑥 ∈ ℂ ↦ {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ ℂ ∧ (𝑦𝑥)𝑓𝑧)})
191, 18wceq 1474 1 wff shift = (𝑓 ∈ V, 𝑥 ∈ ℂ ↦ {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ ℂ ∧ (𝑦𝑥)𝑓𝑧)})
Colors of variables: wff setvar class
This definition is referenced by:  shftfval  13600
  Copyright terms: Public domain W3C validator