Description: Equality theorem for function value. (Contributed by NM, 29Dec1996)
Ref  Expression  

Assertion  fveq2   ( A = B > ( F ` A ) = ( F ` B ) ) 
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  dffv   ( F ` A ) = ( iota x A F x ) 

4  dffv   ( F ` B ) = ( iota x B F x ) 

5  2 3 4  3eqtr4g   ( A = B > ( F ` A ) = ( F ` B ) ) 