Metamath Proof Explorer


Theorem funrnex

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 𝐹𝐵 → ( Fun 𝐹 → ran 𝐹 ∈ V ) )

Proof

Step Hyp Ref Expression
1 funex ( ( Fun 𝐹 ∧ dom 𝐹𝐵 ) → 𝐹 ∈ V )
2 1 ex ( Fun 𝐹 → ( dom 𝐹𝐵𝐹 ∈ V ) )
3 rnexg ( 𝐹 ∈ V → ran 𝐹 ∈ V )
4 2 3 syl6com ( dom 𝐹𝐵 → ( Fun 𝐹 → ran 𝐹 ∈ V ) )