Theorem feqresmpt

Description: Express a restricted function as a mapping. (Contributed by Mario Carneiro, 18-May-2016)

	Ref	Expression
Hypotheses	feqmptd.1	$$⊢\phi \to F:A⟶B$$
	feqresmpt.2	$$⊢\phi \to C\subseteq A$$
Assertion	feqresmpt	$$⊢\phi \to {F\upharpoonright }_C=\left(x\in C⟼F\left(x\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		feqmptd.1	$$⊢\phi \to F:A⟶B$$
2		feqresmpt.2	$$⊢\phi \to C\subseteq A$$
3	1 2	fssresd	$$⊢\phi \to \left({F\upharpoonright }_C\right):C⟶B$$
4	3	feqmptd	$$⊢\phi \to {F\upharpoonright }_C=\left(x\in C⟼\left({F\upharpoonright }_C\right)\left(x\right)\right)$$
5		fvres	$$⊢x\in C\to \left({F\upharpoonright }_C\right)\left(x\right)=F\left(x\right)$$
6	5	mpteq2ia	$$⊢\left(x\in C⟼\left({F\upharpoonright }_C\right)\left(x\right)\right)=\left(x\in C⟼F\left(x\right)\right)$$
7	4 6	eqtrdi	$$⊢\phi \to {F\upharpoonright }_C=\left(x\in C⟼F\left(x\right)\right)$$