Metamath Proof Explorer


Theorem fveq1i

Description: Equality inference for function value. (Contributed by NM, 2-Sep-2003)

Ref Expression
Hypothesis fveq1i.1 𝐹 = 𝐺
Assertion fveq1i ( 𝐹𝐴 ) = ( 𝐺𝐴 )

Proof

Step Hyp Ref Expression
1 fveq1i.1 𝐹 = 𝐺
2 fveq1 ( 𝐹 = 𝐺 → ( 𝐹𝐴 ) = ( 𝐺𝐴 ) )
3 1 2 ax-mp ( 𝐹𝐴 ) = ( 𝐺𝐴 )