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

Metamath Proof Explorer

Theorem imaexd

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

		Ref	Expression
	Hypothesis	rnexd.1	$⊢ φ \to A \in V$
	Assertion	imaexd	$⊢ φ \to A [B] \in V$

Step	Hyp	Ref	Expression
1		rnexd.1	$⊢ φ \to A \in V$
2		imaexg	$⊢ A \in V \to A [B] \in V$
3	1 2	syl	$⊢ φ \to A [B] \in V$