Theorem afveq12d

Description: Equality deduction for function value, analogous to fveq12d . (Contributed by Alexander van der Vekens, 26-May-2017)

	Ref	Expression
Hypotheses	afveq12d.1	$$⊢\phi \to F=G$$
	afveq12d.2	$$⊢\phi \to A=B$$
Assertion	afveq12d	$$⊢\phi \to \left(F\mathrm{\text{'}\text{'}\text{'}}A\right)=\left(G\mathrm{\text{'}\text{'}\text{'}}B\right)$$

Proof

Step	Hyp	Ref	Expression
1		afveq12d.1	$$⊢\phi \to F=G$$
2		afveq12d.2	$$⊢\phi \to A=B$$
3	1 2	dfateq12d	$$⊢\phi \to \left(F\mathrm{defAt}A\leftrightarrow G\mathrm{defAt}B\right)$$
4	1 2	fveq12d	$$⊢\phi \to F\left(A\right)=G\left(B\right)$$
5	3 4	ifbieq1d	$$⊢\phi \to if\left(F\mathrm{defAt}A,F\left(A\right),\mathrm{V}\right)=if\left(G\mathrm{defAt}B,G\left(B\right),\mathrm{V}\right)$$
6		dfafv2	$$⊢\left(F\mathrm{\text{'}\text{'}\text{'}}A\right)=if\left(F\mathrm{defAt}A,F\left(A\right),\mathrm{V}\right)$$
7		dfafv2	$$⊢\left(G\mathrm{\text{'}\text{'}\text{'}}B\right)=if\left(G\mathrm{defAt}B,G\left(B\right),\mathrm{V}\right)$$
8	5 6 7	3eqtr4g	$$⊢\phi \to \left(F\mathrm{\text{'}\text{'}\text{'}}A\right)=\left(G\mathrm{\text{'}\text{'}\text{'}}B\right)$$