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 φ A V
Assertion rnexd φ ran A V

Proof

Step Hyp Ref Expression
1 rnexd.1 φ A V
2 rnexg A V ran A V
3 1 2 syl φ ran A V