Metamath Proof Explorer


Theorem fveq12i

Description: Equality deduction for function value. (Contributed by FL, 27-Jun-2014)

Ref Expression
Hypotheses fveq12i.1 F=G
fveq12i.2 A=B
Assertion fveq12i FA=GB

Proof

Step Hyp Ref Expression
1 fveq12i.1 F=G
2 fveq12i.2 A=B
3 1 fveq1i FA=GA
4 2 fveq2i GA=GB
5 3 4 eqtri FA=GB