Metamath Proof Explorer

Theorem fveq1

Description: Equality theorem for function value. (Contributed by NM, 29-Dec-1996)

Ref Expression
Assertion fveq1 
|- ( F = G -> ( F ` A ) = ( G ` A ) )

Proof

Step Hyp Ref Expression
1 breq 
 |-  ( F = G -> ( A F x <-> A G x ) )
2 1 iotabidv 
 |-  ( F = G -> ( iota x A F x ) = ( iota x A G x ) )
3 df-fv 
 |-  ( F ` A ) = ( iota x A F x )
4 df-fv 
 |-  ( G ` A ) = ( iota x A G x )
5 2 3 4 3eqtr4g 
 |-  ( F = G -> ( F ` A ) = ( G ` A ) )