Description: If the domain of a function exists, so does its range. Part of Theorem 4.15(v) of Monk1 p. 46. This theorem is derived using the Axiom of Replacement in the form of funex . (Contributed by NM, 11-Nov-1995)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | funrnex | |- ( dom F e. B -> ( Fun F -> ran F e. _V ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | funex | |- ( ( Fun F /\ dom F e. B ) -> F e. _V ) |
|
| 2 | 1 | ex | |- ( Fun F -> ( dom F e. B -> F e. _V ) ) |
| 3 | rnexg | |- ( F e. _V -> ran F e. _V ) |
|
| 4 | 2 3 | syl6com | |- ( dom F e. B -> ( Fun F -> ran F e. _V ) ) |