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 φxABV
rnmptssrn.y φxAyCB=D
Assertion rnmptssrn φranxABranyCD

Proof

Step Hyp Ref Expression
1 rnmptssrn.b φxABV
2 rnmptssrn.y φxAyCB=D
3 eqid yCD=yCD
4 3 2 1 elrnmptd φxABranyCD
5 4 ralrimiva φxABranyCD
6 eqid xAB=xAB
7 6 rnmptss xABranyCDranxABranyCD
8 5 7 syl φranxABranyCD