This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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	$⊢ φ \to A \in V$
	Assertion	rnexd	$⊢ φ \to ran A \in V$

Step	Hyp	Ref	Expression
1		rnexd.1	$⊢ φ \to A \in V$
2		rnexg	$⊢ A \in V \to ran A \in V$
3	1 2	syl	$⊢ φ \to ran A \in V$