Metamath Proof Explorer

Theorem fveq1i

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

Ref Expression
Hypothesis fveq1i.1 
|- F = G
Assertion fveq1i 
|- ( F ` A ) = ( G ` A )

Proof

Step Hyp Ref Expression
1 fveq1i.1 
 |-  F = G
2 fveq1 
 |-  ( F = G -> ( F ` A ) = ( G ` A ) )
3 1 2 ax-mp 
 |-  ( F ` A ) = ( G ` A )