Metamath Proof Explorer


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 FV
Assertion shftidt AFshift0A=FA

Proof

Step Hyp Ref Expression
1 shftfval.1 FV
2 1 shftidt2 Fshift0=F
3 2 fveq1i Fshift0A=FA
4 fvres AFA=FA
5 3 4 eqtrid AFshift0A=FA