Description: Inclusion relation for two ranges expressed in maps-to notation. (Contributed by Glauco Siliprandi, 17-Aug-2020)
Ref | Expression | ||
---|---|---|---|
Hypotheses | rnmptssrn.b | |
|
rnmptssrn.y | |
||
Assertion | rnmptssrn | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rnmptssrn.b | |
|
2 | rnmptssrn.y | |
|
3 | eqid | |
|
4 | 3 2 1 | elrnmptd | |
5 | 4 | ralrimiva | |
6 | eqid | |
|
7 | 6 | rnmptss | |
8 | 5 7 | syl | |