Theorem rnmptssrn

Description: Inclusion relation for two ranges expressed in maps-to notation. (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Hypotheses	rnmptssrn.b	|- ( ( ph /\ x e. A ) -> B e. V )
	rnmptssrn.y	|- ( ( ph /\ x e. A ) -> E. y e. C B = D )
Assertion	rnmptssrn	|- ( ph -> ran ( x e. A |-> B ) C_ ran ( y e. C |-> D ) )

Proof

Step	Hyp	Ref	Expression
1		rnmptssrn.b	|- ( ( ph /\ x e. A ) -> B e. V )
2		rnmptssrn.y	|- ( ( ph /\ x e. A ) -> E. y e. C B = D )
3		eqid	|- ( y e. C |-> D ) = ( y e. C |-> D )
4	3 2 1	elrnmptd	|- ( ( ph /\ x e. A ) -> B e. ran ( y e. C |-> D ) )
5	4	ralrimiva	|- ( ph -> A. x e. A B e. ran ( y e. C |-> D ) )
6		eqid	|- ( x e. A |-> B ) = ( x e. A |-> B )
7	6	rnmptss	|- ( A. x e. A B e. ran ( y e. C |-> D ) -> ran ( x e. A |-> B ) C_ ran ( y e. C |-> D ) )
8	5 7	syl	|- ( ph -> ran ( x e. A |-> B ) C_ ran ( y e. C |-> D ) )