Description: Membership in the range of a function. (Contributed by NM, 30-Aug-2004) (Revised by Mario Carneiro, 31-Aug-2015)
Ref | Expression | ||
---|---|---|---|
Hypotheses | rnmpt.1 | |
|
elrnmpti.2 | |
||
Assertion | elrnmpti | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rnmpt.1 | |
|
2 | elrnmpti.2 | |
|
3 | 2 | rgenw | |
4 | 1 | elrnmptg | |
5 | 3 4 | ax-mp | |