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\to \left(F\mathrm{\text{'}\text{'}\text{'}}A\right)=\left(F\mathrm{\text{'}\text{'}\text{'}}B\right)$$

Proof

Step	Hyp	Ref	Expression
1		eqidd	$$⊢A=B\to F=F$$
2		id	$$⊢A=B\to A=B$$
3	1 2	afveq12d	$$⊢A=B\to \left(F\mathrm{\text{'}\text{'}\text{'}}A\right)=\left(F\mathrm{\text{'}\text{'}\text{'}}B\right)$$