Metamath Proof Explorer


Theorem shftvalg

Description: Value of a sequence shifted by A . (Contributed by Scott Fenton, 16-Dec-2017)

Ref Expression
Assertion shftvalg F V A B F shift A B = F B A

Proof

Step Hyp Ref Expression
1 oveq1 f = F f shift A = F shift A
2 1 fveq1d f = F f shift A B = F shift A B
3 fveq1 f = F f B A = F B A
4 2 3 eqeq12d f = F f shift A B = f B A F shift A B = F B A
5 4 imbi2d f = F A B f shift A B = f B A A B F shift A B = F B A
6 vex f V
7 6 shftval A B f shift A B = f B A
8 5 7 vtoclg F V A B F shift A B = F B A
9 8 3impib F V A B F shift A B = F B A