Metamath Proof Explorer


Theorem rnexd

Description: The range of a set is a set. Deduction version of rnexd . (Contributed by Thierry Arnoux, 14-Feb-2025)

Ref Expression
Hypothesis rnexd.1 ( 𝜑𝐴𝑉 )
Assertion rnexd ( 𝜑 → ran 𝐴 ∈ V )

Proof

Step Hyp Ref Expression
1 rnexd.1 ( 𝜑𝐴𝑉 )
2 rnexg ( 𝐴𝑉 → ran 𝐴 ∈ V )
3 1 2 syl ( 𝜑 → ran 𝐴 ∈ V )