Theorem shftidt

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

	Ref	Expression
Hypothesis	shftfval.1	|- F e. _V
Assertion	shftidt	|- ( A e. CC -> ( ( F shift 0 ) ` A ) = ( F ` A ) )

Proof

Step	Hyp	Ref	Expression
1		shftfval.1	|- F e. _V
2	1	shftidt2	|- ( F shift 0 ) = ( F |` CC )
3	2	fveq1i	|- ( ( F shift 0 ) ` A ) = ( ( F |` CC ) ` A )
4		fvres	|- ( A e. CC -> ( ( F |` CC ) ` A ) = ( F ` A ) )
5	3 4	syl5eq	|- ( A e. CC -> ( ( F shift 0 ) ` A ) = ( F ` A ) )