Theorem sepexlem

Description: Lemma for sepex . Use sepex instead. (Contributed by Matthew House, 19-Sep-2025) (New usage is discouraged.)

	Ref	Expression
Assertion	sepexlem	|- ( E. y A. x ( ph -> x e. y ) -> E. z A. x ( x e. z <-> ph ) )

Proof

Step	Hyp	Ref	Expression
1		ax-sep	|- E. z A. x ( x e. z <-> ( x e. y /\ ph ) )
2		bimsc1	|- ( ( ( ph -> x e. y ) /\ ( x e. z <-> ( x e. y /\ ph ) ) ) -> ( x e. z <-> ph ) )
3	2	ex	|- ( ( ph -> x e. y ) -> ( ( x e. z <-> ( x e. y /\ ph ) ) -> ( x e. z <-> ph ) ) )
4	3	al2imi	|- ( A. x ( ph -> x e. y ) -> ( A. x ( x e. z <-> ( x e. y /\ ph ) ) -> A. x ( x e. z <-> ph ) ) )
5	4	eximdv	|- ( A. x ( ph -> x e. y ) -> ( E. z A. x ( x e. z <-> ( x e. y /\ ph ) ) -> E. z A. x ( x e. z <-> ph ) ) )
6	1 5	mpi	|- ( A. x ( ph -> x e. y ) -> E. z A. x ( x e. z <-> ph ) )
7	6	exlimiv	|- ( E. y A. x ( ph -> x e. y ) -> E. z A. x ( x e. z <-> ph ) )