Theorem rnmptss2

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

	Ref	Expression
Hypotheses	rnmptss2.1	|- F/ x ph
	rnmptss2.3	|- ( ph -> A C_ B )
	rnmptss2.4	|- ( ( ph /\ x e. A ) -> C e. V )
Assertion	rnmptss2	|- ( ph -> ran ( x e. A |-> C ) C_ ran ( x e. B |-> C ) )

Proof

Step	Hyp	Ref	Expression
1		rnmptss2.1	|- F/ x ph
2		rnmptss2.3	|- ( ph -> A C_ B )
3		rnmptss2.4	|- ( ( ph /\ x e. A ) -> C e. V )
4		nfmpt1	|- F/_ x ( x e. B |-> C )
5	4	nfrn	|- F/_ x ran ( x e. B |-> C )
6		eqid	|- ( x e. A |-> C ) = ( x e. A |-> C )
7		eqid	|- ( x e. B |-> C ) = ( x e. B |-> C )
8	2	sselda	|- ( ( ph /\ x e. A ) -> x e. B )
9	7 8 3	elrnmpt1d	|- ( ( ph /\ x e. A ) -> C e. ran ( x e. B |-> C ) )
10	1 5 6 9	rnmptssdf	|- ( ph -> ran ( x e. A |-> C ) C_ ran ( x e. B |-> C ) )