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

Metamath Proof Explorer

Theorem rabexg

Description: Separation Scheme in terms of a restricted class abstraction. (Contributed by NM, 23-Oct-1999) (Proof shortened by BJ, 24-Jul-2025)

		Ref	Expression
	Assertion	rabexg	$⊢ A \in V \to \{x \in A \| φ\} \in V$

Step	Hyp	Ref	Expression
1		rabelpw	$⊢ A \in V \to \{x \in A \| φ\} \in 𝒫 A$
2	1	elexd	$⊢ A \in V \to \{x \in A \| φ\} \in V$