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

Metamath Proof Explorer

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 ) )