Theorem mptss

Description: Sufficient condition for inclusion among two functions in maps-to notation. (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Assertion	mptss	$$⊢A\subseteq B\to \left(x\in A⟼C\right)\subseteq \left(x\in B⟼C\right)$$

Proof

Step	Hyp	Ref	Expression
1		resmpt	$$⊢A\subseteq B\to {\left(x\in B⟼C\right)\upharpoonright }_A=\left(x\in A⟼C\right)$$
2		resss	$$⊢{\left(x\in B⟼C\right)\upharpoonright }_A\subseteq \left(x\in B⟼C\right)$$
3	1 2	eqsstrrdi	$$⊢A\subseteq B\to \left(x\in A⟼C\right)\subseteq \left(x\in B⟼C\right)$$