Theorem afv2eq12d

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

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

Proof

Step	Hyp	Ref	Expression
1		afv2eq12d.1	$$⊢\phi \to F=G$$
2		afv2eq12d.2	$$⊢\phi \to A=B$$
3	1 2	dfateq12d	$$⊢\phi \to \left(F\mathrm{defAt}A\leftrightarrow G\mathrm{defAt}B\right)$$
4		eqidd	$$⊢\phi \to x=x$$
5	2 1 4	breq123d	$$⊢\phi \to \left(AFx\leftrightarrow BGx\right)$$
6	5	iotabidv	$$⊢\phi \to \left(\iota x|AFx\right)=\left(\iota x|BGx\right)$$
7	1	rneqd	$$⊢\phi \to \mathrm{ran}F=\mathrm{ran}G$$
8	7	unieqd	$$⊢\phi \to \bigcup \mathrm{ran}F=\bigcup \mathrm{ran}G$$
9	8	pweqd	$$⊢\phi \to 𝒫\bigcup \mathrm{ran}F=𝒫\bigcup \mathrm{ran}G$$
10	3 6 9	ifbieq12d	$$⊢\phi \to if\left(F\mathrm{defAt}A,\left(\iota x|AFx\right),𝒫\bigcup \mathrm{ran}F\right)=if\left(G\mathrm{defAt}B,\left(\iota x|BGx\right),𝒫\bigcup \mathrm{ran}G\right)$$
11		df-afv2	$$⊢\left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)=if\left(F\mathrm{defAt}A,\left(\iota x|AFx\right),𝒫\bigcup \mathrm{ran}F\right)$$
12		df-afv2	$$⊢\left(G\mathrm{\text{'}\text{'}\text{'}\text{'}}B\right)=if\left(G\mathrm{defAt}B,\left(\iota x|BGx\right),𝒫\bigcup \mathrm{ran}G\right)$$
13	10 11 12	3eqtr4g	$$⊢\phi \to \left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)=\left(G\mathrm{\text{'}\text{'}\text{'}\text{'}}B\right)$$