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	|- ( E. y A. x ( ph -> x e. y ) -> E. z A. x ( x e. z <-> ph ) )

Proof

Step	Hyp	Ref	Expression
1		sepexlem	|- ( E. y A. x ( ph -> x e. y ) -> E. w A. x ( x e. w <-> ph ) )
2		biimpr	|- ( ( x e. w <-> ph ) -> ( ph -> x e. w ) )
3	2	alimi	|- ( A. x ( x e. w <-> ph ) -> A. x ( ph -> x e. w ) )
4	3	eximi	|- ( E. w A. x ( x e. w <-> ph ) -> E. w A. x ( ph -> x e. w ) )
5		sepexlem	|- ( E. w A. x ( ph -> x e. w ) -> E. z A. x ( x e. z <-> ph ) )
6	1 4 5	3syl	|- ( E. y A. x ( ph -> x e. y ) -> E. z A. x ( x e. z <-> ph ) )