Description: The range of a set is a set. Corollary 6.8(3) of TakeutiZaring p. 26. Similar to Lemma 3D of Enderton p. 41. (Contributed by NM, 7-Jul-2008)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | dmex.1 | |- A e. _V |
|
| Assertion | rnex | |- ran A e. _V |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | dmex.1 | |- A e. _V |
|
| 2 | rnexg | |- ( A e. _V -> ran A e. _V ) |
|
| 3 | 1 2 | ax-mp | |- ran A e. _V |