This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) )