Theorem afv2eq2

Description: Equality theorem for function value, analogous to fveq2 . (Contributed by AV, 4-Sep-2022)

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