This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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