Metamath Proof Explorer

Theorem afveq2

Description: Equality theorem for function value, analogous to fveq1 . (Contributed by Alexander van der Vekens, 22-Jul-2017)

Ref Expression
Assertion afveq2 
|- ( A = B -> ( F ''' A ) = ( F ''' B ) )

Proof

Step Hyp Ref Expression
1 eqidd 
 |-  ( A = B -> F = F )
2 id 
 |-  ( A = B -> A = B )
3 1 2 afveq12d 
 |-  ( A = B -> ( F ''' A ) = ( F ''' B ) )