Theorem fssresd

Description: Restriction of a function with a subclass of its domain, deduction form. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	fssresd.1	$$⊢\phi \to F:A⟶B$$
	fssresd.2	$$⊢\phi \to C\subseteq A$$
Assertion	fssresd	$$⊢\phi \to \left({F\upharpoonright }_C\right):C⟶B$$

Proof

Step	Hyp	Ref	Expression
1		fssresd.1	$$⊢\phi \to F:A⟶B$$
2		fssresd.2	$$⊢\phi \to C\subseteq A$$
3		fssres	$$⊢\left(F:A⟶B\wedge C\subseteq A\right)\to \left({F\upharpoonright }_C\right):C⟶B$$
4	1 2 3	syl2anc	$$⊢\phi \to \left({F\upharpoonright }_C\right):C⟶B$$