Theorem shftidt2

Description: Identity law for the shift operation. (Contributed by Mario Carneiro, 5-Nov-2013)

	Ref	Expression
Hypothesis	shftfval.1	$$⊢F\in \mathrm{V}$$
Assertion	shftidt2	$$⊢F\mathrm{shift}0={F\upharpoonright }_{ℂ}$$

Proof

Step	Hyp	Ref	Expression
1		shftfval.1	$$⊢F\in \mathrm{V}$$
2		subid1	$$⊢x\in ℂ\to x-0=x$$
3	2	breq1d	$$⊢x\in ℂ\to \left(\left(x-0\right)Fy\leftrightarrow xFy\right)$$
4	3	pm5.32i	$$⊢\left(x\in ℂ\wedge \left(x-0\right)Fy\right)\leftrightarrow \left(x\in ℂ\wedge xFy\right)$$
5	4	opabbii	$$⊢\left\{⟨x,y⟩|\left(x\in ℂ\wedge \left(x-0\right)Fy\right)\right\}=\left\{⟨x,y⟩|\left(x\in ℂ\wedge xFy\right)\right\}$$
6		0cn	$$⊢0\in ℂ$$
7	1	shftfval	$$⊢0\in ℂ\to F\mathrm{shift}0=\left\{⟨x,y⟩|\left(x\in ℂ\wedge \left(x-0\right)Fy\right)\right\}$$
8	6 7	ax-mp	$$⊢F\mathrm{shift}0=\left\{⟨x,y⟩|\left(x\in ℂ\wedge \left(x-0\right)Fy\right)\right\}$$
9		dfres2	$$⊢{F\upharpoonright }_{ℂ}=\left\{⟨x,y⟩|\left(x\in ℂ\wedge xFy\right)\right\}$$
10	5 8 9	3eqtr4i	$$⊢F\mathrm{shift}0={F\upharpoonright }_{ℂ}$$