Theorem feqresmptf

Description: Express a restricted function as a mapping. (Contributed by Glauco Siliprandi, 23-Oct-2021)

	Ref	Expression
Hypotheses	feqresmptf.1	$$⊢\underset{\_}{Ⅎ}xF$$
	feqresmptf.2	$$⊢\phi \to F:A⟶B$$
	feqresmptf.3	$$⊢\phi \to C\subseteq A$$
Assertion	feqresmptf	$$⊢\phi \to {F\upharpoonright }_C=\left(x\in C⟼F\left(x\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		feqresmptf.1	$$⊢\underset{\_}{Ⅎ}xF$$
2		feqresmptf.2	$$⊢\phi \to F:A⟶B$$
3		feqresmptf.3	$$⊢\phi \to C\subseteq A$$
4		nfcv	$$⊢\underset{\_}{Ⅎ}xC$$
5	1 4	nfres	$$⊢\underset{\_}{Ⅎ}x\left({F\upharpoonright }_C\right)$$
6	2 3	fssresd	$$⊢\phi \to \left({F\upharpoonright }_C\right):C⟶B$$
7	4 5 6	feqmptdf	$$⊢\phi \to {F\upharpoonright }_C=\left(x\in C⟼\left({F\upharpoonright }_C\right)\left(x\right)\right)$$
8		fvres	$$⊢x\in C\to \left({F\upharpoonright }_C\right)\left(x\right)=F\left(x\right)$$
9	8	mpteq2ia	$$⊢\left(x\in C⟼\left({F\upharpoonright }_C\right)\left(x\right)\right)=\left(x\in C⟼F\left(x\right)\right)$$
10	7 9	eqtrdi	$$⊢\phi \to {F\upharpoonright }_C=\left(x\in C⟼F\left(x\right)\right)$$