Metamath Proof Explorer

Theorem fveqeq2

Description: Equality deduction for function value. (Contributed by BJ, 31-Aug-2022)

Ref Expression
Assertion fveqeq2 
|- ( A = B -> ( ( F ` A ) = C <-> ( F ` B ) = C ) )

Proof

Step Hyp Ref Expression
1 id 
 |-  ( A = B -> A = B )
2 1 fveqeq2d 
 |-  ( A = B -> ( ( F ` A ) = C <-> ( F ` B ) = C ) )