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

Metamath Proof Explorer

Theorem imaexi

Description: The image of a set is a set. (Contributed by Glauco Siliprandi, 26-Jun-2021) (Proof shortened by SN, 27-Apr-2025)

		Ref	Expression
	Hypothesis	imaexi.1	$⊢ A \in V$
	Assertion	imaexi	$⊢ A [B] \in V$

Step	Hyp	Ref	Expression
1		imaexi.1	$⊢ A \in V$
2	1	elexi	$⊢ A \in V$
3	2	imaex	$⊢ A [B] \in V$