Theorem fnssresd

Description: Restriction of a function to a subclass of its domain. (Contributed by Glauco Siliprandi, 5-Feb-2022)

	Ref	Expression
Hypotheses	fnssresd.1	$$⊢\phi \to FFnA$$
	fnssresd.2	$$⊢\phi \to B\subseteq A$$
Assertion	fnssresd	$$⊢\phi \to \left({F\upharpoonright }_B\right)FnB$$

Proof

Step	Hyp	Ref	Expression
1		fnssresd.1	$$⊢\phi \to FFnA$$
2		fnssresd.2	$$⊢\phi \to B\subseteq A$$
3		fnssres	$$⊢\left(FFnA\wedge B\subseteq A\right)\to \left({F\upharpoonright }_B\right)FnB$$
4	1 2 3	syl2anc	$$⊢\phi \to \left({F\upharpoonright }_B\right)FnB$$