Theorem dfateq12d

Description: Equality deduction for "defined at". (Contributed by Alexander van der Vekens, 26-May-2017)

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

Proof

Step	Hyp	Ref	Expression
1		dfateq12d.1	$$⊢\phi \to F=G$$
2		dfateq12d.2	$$⊢\phi \to A=B$$
3	1	dmeqd	$$⊢\phi \to \mathrm{dom}F=\mathrm{dom}G$$
4	2 3	eleq12d	$$⊢\phi \to \left(A\in \mathrm{dom}F\leftrightarrow B\in \mathrm{dom}G\right)$$
5	2	sneqd	$$⊢\phi \to \left\{A\right\}=\left\{B\right\}$$
6	1 5	reseq12d	$$⊢\phi \to {F\upharpoonright }_{\left\{A\right\}}={G\upharpoonright }_{\left\{B\right\}}$$
7	6	funeqd	$$⊢\phi \to \left(\mathrm{Fun}\left({F\upharpoonright }_{\left\{A\right\}}\right)\leftrightarrow \mathrm{Fun}\left({G\upharpoonright }_{\left\{B\right\}}\right)\right)$$
8	4 7	anbi12d	$$⊢\phi \to \left(\left(A\in \mathrm{dom}F\wedge \mathrm{Fun}\left({F\upharpoonright }_{\left\{A\right\}}\right)\right)\leftrightarrow \left(B\in \mathrm{dom}G\wedge \mathrm{Fun}\left({G\upharpoonright }_{\left\{B\right\}}\right)\right)\right)$$
9		df-dfat	$$⊢F\mathrm{defAt}A\leftrightarrow \left(A\in \mathrm{dom}F\wedge \mathrm{Fun}\left({F\upharpoonright }_{\left\{A\right\}}\right)\right)$$
10		df-dfat	$$⊢G\mathrm{defAt}B\leftrightarrow \left(B\in \mathrm{dom}G\wedge \mathrm{Fun}\left({G\upharpoonright }_{\left\{B\right\}}\right)\right)$$
11	8 9 10	3bitr4g	$$⊢\phi \to \left(F\mathrm{defAt}A\leftrightarrow G\mathrm{defAt}B\right)$$