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

Metamath Proof Explorer

Theorem fveq12d

Description: Equality deduction for function value. (Contributed by FL, 22-Dec-2008)

Ref Expression
Hypotheses fveq12d.1 ⊢ φ → F = G
fveq12d.2 ⊢ φ → A = B
Assertion fveq12d ⊢ φ → F ⁡ A = G ⁡ B

Proof

Step Hyp Ref Expression
1 fveq12d.1 ⊢ φ → F = G
2 fveq12d.2 ⊢ φ → A = B
3 1 fveq1d ⊢ φ → F ⁡ A = G ⁡ A
4 2 fveq2d ⊢ φ → G ⁡ A = G ⁡ B
5 3 4 eqtrd ⊢ φ → F ⁡ A = G ⁡ B