Description: The range of a function in maps-to notation. (Contributed by Glauco Siliprandi, 17-Aug-2020)
Ref | Expression | ||
---|---|---|---|
Hypotheses | elrnmptd.f | ||
elrnmptd.x | |||
elrnmptd.c | |||
Assertion | elrnmptd |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elrnmptd.f | ||
2 | elrnmptd.x | ||
3 | elrnmptd.c | ||
4 | 1 | elrnmpt | |
5 | 3 4 | syl | |
6 | 2 5 | mpbird |