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

Metamath Proof Explorer

Theorem abex

Description: Conditions for a class abstraction to be a set. Remark: This proof is shorter than a proof using abexd . (Contributed by AV, 19-Apr-2025)

	Ref	Expression
Hypotheses	abex.1	$⊢ φ \to x \in A$
	abex.2	$⊢ A \in V$
Assertion	abex	$⊢ \{x \| φ\} \in V$

Proof

Step	Hyp	Ref	Expression
1		abex.1	$⊢ φ \to x \in A$
2		abex.2	$⊢ A \in V$
3	1	abssi	$⊢ \{x \| φ\} \subseteq A$
4	2 3	ssexi	$⊢ \{x \| φ\} \in V$