Theorem rnmptss2

Description: The range of a function given by the maps-to notation as a subset. (Contributed by Glauco Siliprandi, 23-Oct-2021)

	Ref	Expression
Hypotheses	rnmptss2.1	$$⊢Ⅎx\phi$$
	rnmptss2.3	$$⊢\phi \to A\subseteq B$$
	rnmptss2.4	$$⊢\left(\phi \wedge x\in A\right)\to C\in V$$
Assertion	rnmptss2	$$⊢\phi \to \mathrm{ran}\left(x\in A⟼C\right)\subseteq \mathrm{ran}\left(x\in B⟼C\right)$$

Proof

Step	Hyp	Ref	Expression
1		rnmptss2.1	$$⊢Ⅎx\phi$$
2		rnmptss2.3	$$⊢\phi \to A\subseteq B$$
3		rnmptss2.4	$$⊢\left(\phi \wedge x\in A\right)\to C\in V$$
4		nfmpt1	$$⊢\underset{\_}{Ⅎ}x\left(x\in B⟼C\right)$$
5	4	nfrn	$$⊢\underset{\_}{Ⅎ}x\mathrm{ran}\left(x\in B⟼C\right)$$
6		eqid	$$⊢\left(x\in A⟼C\right)=\left(x\in A⟼C\right)$$
7		eqid	$$⊢\left(x\in B⟼C\right)=\left(x\in B⟼C\right)$$
8	2	sselda	$$⊢\left(\phi \wedge x\in A\right)\to x\in B$$
9	7 8 3	elrnmpt1d	$$⊢\left(\phi \wedge x\in A\right)\to C\in \mathrm{ran}\left(x\in B⟼C\right)$$
10	1 5 6 9	rnmptssdf	$$⊢\phi \to \mathrm{ran}\left(x\in A⟼C\right)\subseteq \mathrm{ran}\left(x\in B⟼C\right)$$