Definition df-shft

Description: Define a function shifter. This operation offsets the value argument of a function (ordinarily on a subset of CC ) and produces a new function on CC . See shftval for its value. (Contributed by NM, 20-Jul-2005)

	Ref	Expression
Assertion	df-shft	$$⊢\mathrm{shift}=\left(f\in \mathrm{V},x\in ℂ⟼\left\{⟨y,z⟩|\left(y\in ℂ\wedge \left(y-x\right)fz\right)\right\}\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cshi	$$class\mathrm{shift}$$
1		vf	$$setvarf$$
2		cvv	$$class\mathrm{V}$$
3		vx	$$setvarx$$
4		cc	$$classℂ$$
5		vy	$$setvary$$
6		vz	$$setvarz$$
7	5	cv	$$setvary$$
8	7 4	wcel	$$wffy\in ℂ$$
9		cmin	$$class-$$
10	3	cv	$$setvarx$$
11	7 10 9	co	$$class\left(y-x\right)$$
12	1	cv	$$setvarf$$
13	6	cv	$$setvarz$$
14	11 13 12	wbr	$$wff\left(y-x\right)fz$$
15	8 14	wa	$$wff\left(y\in ℂ\wedge \left(y-x\right)fz\right)$$
16	15 5 6	copab	$$class\left\{⟨y,z⟩|\left(y\in ℂ\wedge \left(y-x\right)fz\right)\right\}$$
17	1 3 2 4 16	cmpo	$$class\left(f\in \mathrm{V},x\in ℂ⟼\left\{⟨y,z⟩|\left(y\in ℂ\wedge \left(y-x\right)fz\right)\right\}\right)$$
18	0 17	wceq	$$wff\mathrm{shift}=\left(f\in \mathrm{V},x\in ℂ⟼\left\{⟨y,z⟩|\left(y\in ℂ\wedge \left(y-x\right)fz\right)\right\}\right)$$