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 ( 𝐴 = 𝐵 → ( 𝐹 ''' 𝐴 ) = ( 𝐹 ''' 𝐵 ) )

Proof

Step Hyp Ref Expression
1 eqidd ( 𝐴 = 𝐵𝐹 = 𝐹 )
2 id ( 𝐴 = 𝐵𝐴 = 𝐵 )
3 1 2 afveq12d ( 𝐴 = 𝐵 → ( 𝐹 ''' 𝐴 ) = ( 𝐹 ''' 𝐵 ) )