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 F A = G B

Proof

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