Theorem sepex

Description: Convert implication to equivalence within an existence statement using the Separation Scheme (Aussonderung) ax-sep . Similar to Theorem 1.3(ii) of BellMachover p. 463. (Contributed by Matthew House, 19-Sep-2025)

	Ref	Expression
Assertion	sepex	$$⊢\exists y\forall x\left(\phi \to x\in y\right)\to \exists z\forall x\left(x\in z\leftrightarrow \phi \right)$$

Proof

Step	Hyp	Ref	Expression
1		sepexlem	$$⊢\exists y\forall x\left(\phi \to x\in y\right)\to \exists w\forall x\left(x\in w\leftrightarrow \phi \right)$$
2		biimpr	$$⊢\left(x\in w\leftrightarrow \phi \right)\to \left(\phi \to x\in w\right)$$
3	2	alimi	$$⊢\forall x\left(x\in w\leftrightarrow \phi \right)\to \forall x\left(\phi \to x\in w\right)$$
4	3	eximi	$$⊢\exists w\forall x\left(x\in w\leftrightarrow \phi \right)\to \exists w\forall x\left(\phi \to x\in w\right)$$
5		sepexlem	$$⊢\exists w\forall x\left(\phi \to x\in w\right)\to \exists z\forall x\left(x\in z\leftrightarrow \phi \right)$$
6	1 4 5	3syl	$$⊢\exists y\forall x\left(\phi \to x\in y\right)\to \exists z\forall x\left(x\in z\leftrightarrow \phi \right)$$