Theorem sepexi

Description: Convert implication to equivalence within an existence statement using the Separation Scheme (Aussonderung) ax-sep . Inference associated with sepex . (Contributed by NM, 21-Jun-1993) Generalize conclusion, extract closed form, and avoid ax-9 . (Revised by Matthew House, 19-Sep-2025)

	Ref	Expression
Hypothesis	sepexi.1	$$⊢\exists y\forall x\left(\phi \to x\in y\right)$$
Assertion	sepexi	$$⊢\exists z\forall x\left(x\in z\leftrightarrow \phi \right)$$

Proof

Step	Hyp	Ref	Expression
1		sepexi.1	$$⊢\exists y\forall x\left(\phi \to x\in y\right)$$
2		sepex	$$⊢\exists y\forall x\left(\phi \to x\in y\right)\to \exists z\forall x\left(x\in z\leftrightarrow \phi \right)$$
3	1 2	ax-mp	$$⊢\exists z\forall x\left(x\in z\leftrightarrow \phi \right)$$