Theorem fresin2

Description: Restriction of a function with respect to the intersection with its domain. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Assertion	fresin2	$$⊢F:A⟶B\to {F\upharpoonright }_{\left(C\cap A\right)}={F\upharpoonright }_C$$

Proof

Step	Hyp	Ref	Expression
1		fdm	$$⊢F:A⟶B\to \mathrm{dom}F=A$$
2	1	eqcomd	$$⊢F:A⟶B\to A=\mathrm{dom}F$$
3	2	ineq2d	$$⊢F:A⟶B\to C\cap A=C\cap \mathrm{dom}F$$
4	3	reseq2d	$$⊢F:A⟶B\to {F\upharpoonright }_{\left(C\cap A\right)}={F\upharpoonright }_{\left(C\cap \mathrm{dom}F\right)}$$
5		frel	$$⊢F:A⟶B\to \mathrm{Rel}F$$
6		resindm	$$⊢\mathrm{Rel}F\to {F\upharpoonright }_{\left(C\cap \mathrm{dom}F\right)}={F\upharpoonright }_C$$
7	5 6	syl	$$⊢F:A⟶B\to {F\upharpoonright }_{\left(C\cap \mathrm{dom}F\right)}={F\upharpoonright }_C$$
8	4 7	eqtrd	$$⊢F:A⟶B\to {F\upharpoonright }_{\left(C\cap A\right)}={F\upharpoonright }_C$$