Description: Equality deduction for function value. (Contributed by BJ, 31Aug2022)
Ref  Expression  

Assertion  fveqeq2   ( A = B > ( ( F ` A ) = C <> ( F ` B ) = C ) ) 
Step  Hyp  Ref  Expression 

1  id   ( A = B > A = B ) 

2  1  fveqeq2d   ( A = B > ( ( F ` A ) = C <> ( F ` B ) = C ) ) 