Metamath Proof Explorer


Theorem rnex

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 𝐴 ∈ V
Assertion rnex ran 𝐴 ∈ V

Proof

Step Hyp Ref Expression
1 dmex.1 𝐴 ∈ V
2 rnexg ( 𝐴 ∈ V → ran 𝐴 ∈ V )
3 1 2 ax-mp ran 𝐴 ∈ V