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 φ$
	rnmptss2.3	$⊢ φ \to A \subseteq B$
	rnmptss2.4	$⊢ (φ \land x \in A) \to C \in V$
Assertion	rnmptss2	$⊢ φ \to ran (x \in A ⟼ C) \subseteq ran (x \in B ⟼ C)$

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

Metamath Proof Explorer