Metamath Proof Explorer

Theorem fveq2

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

Ref Expression
Assertion fveq2 
|- ( A = B -> ( F ` A ) = ( F ` B ) )

Proof

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