Theorem shftidt2

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

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

Proof

Step	Hyp	Ref	Expression
1		shftfval.1	|- F e. _V
2		subid1	|- ( x e. CC -> ( x - 0 ) = x )
3	2	breq1d	|- ( x e. CC -> ( ( x - 0 ) F y <-> x F y ) )
4	3	pm5.32i	|- ( ( x e. CC /\ ( x - 0 ) F y ) <-> ( x e. CC /\ x F y ) )
5	4	opabbii	|- { <. x , y >. | ( x e. CC /\ ( x - 0 ) F y ) } = { <. x , y >. | ( x e. CC /\ x F y ) }
6		0cn	|- 0 e. CC
7	1	shftfval	|- ( 0 e. CC -> ( F shift 0 ) = { <. x , y >. | ( x e. CC /\ ( x - 0 ) F y ) } )
8	6 7	ax-mp	|- ( F shift 0 ) = { <. x , y >. | ( x e. CC /\ ( x - 0 ) F y ) }
9		dfres2	|- ( F |` CC ) = { <. x , y >. | ( x e. CC /\ x F y ) }
10	5 8 9	3eqtr4i	|- ( F shift 0 ) = ( F |` CC )