Theorem fresin

Description: An identity for the mapping relationship under restriction. (Contributed by Scott Fenton, 4-Sep-2011) (Proof shortened by Mario Carneiro, 26-May-2016)

	Ref	Expression
Assertion	fresin	$$⊢F:A⟶B\to \left({F\upharpoonright }_X\right):A\cap X⟶B$$

Proof

Step	Hyp	Ref	Expression
1		inss1	$$⊢A\cap X\subseteq A$$
2		fssres	$$⊢\left(F:A⟶B\wedge A\cap X\subseteq A\right)\to \left({F\upharpoonright }_{\left(A\cap X\right)}\right):A\cap X⟶B$$
3	1 2	mpan2	$$⊢F:A⟶B\to \left({F\upharpoonright }_{\left(A\cap X\right)}\right):A\cap X⟶B$$
4		resres	$$⊢{\left({F\upharpoonright }_A\right)\upharpoonright }_X={F\upharpoonright }_{\left(A\cap X\right)}$$
5		ffn	$$⊢F:A⟶B\to FFnA$$
6		fnresdm	$$⊢FFnA\to {F\upharpoonright }_A=F$$
7	5 6	syl	$$⊢F:A⟶B\to {F\upharpoonright }_A=F$$
8	7	reseq1d	$$⊢F:A⟶B\to {\left({F\upharpoonright }_A\right)\upharpoonright }_X={F\upharpoonright }_X$$
9	4 8	eqtr3id	$$⊢F:A⟶B\to {F\upharpoonright }_{\left(A\cap X\right)}={F\upharpoonright }_X$$
10	9	feq1d	$$⊢F:A⟶B\to \left(\left({F\upharpoonright }_{\left(A\cap X\right)}\right):A\cap X⟶B\leftrightarrow \left({F\upharpoonright }_X\right):A\cap X⟶B\right)$$
11	3 10	mpbid	$$⊢F:A⟶B\to \left({F\upharpoonright }_X\right):A\cap X⟶B$$