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

Metamath Proof Explorer

Theorem bm1.3iiOLD

Description: Obsolete version of sepexi as of 18-Sep-2025. (Contributed by NM, 21-Jun-1993) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypothesis bm1.3iiOLD.1 
|- E. x A. y ( ph -> y e. x )
Assertion bm1.3iiOLD 
|- E. x A. y ( y e. x <-> ph )

Proof

Step Hyp Ref Expression
1 bm1.3iiOLD.1 
 |-  E. x A. y ( ph -> y e. x )
2 19.42v 
 |-  ( E. x ( A. y ( ph -> y e. z ) /\ A. y ( y e. x <-> ( y e. z /\ ph ) ) ) <-> ( A. y ( ph -> y e. z ) /\ E. x A. y ( y e. x <-> ( y e. z /\ ph ) ) ) )
3 bimsc1 
 |-  ( ( ( ph -> y e. z ) /\ ( y e. x <-> ( y e. z /\ ph ) ) ) -> ( y e. x <-> ph ) )
4 3 alanimi 
 |-  ( ( A. y ( ph -> y e. z ) /\ A. y ( y e. x <-> ( y e. z /\ ph ) ) ) -> A. y ( y e. x <-> ph ) )
5 4 eximi 
 |-  ( E. x ( A. y ( ph -> y e. z ) /\ A. y ( y e. x <-> ( y e. z /\ ph ) ) ) -> E. x A. y ( y e. x <-> ph ) )
6 2 5 sylbir 
 |-  ( ( A. y ( ph -> y e. z ) /\ E. x A. y ( y e. x <-> ( y e. z /\ ph ) ) ) -> E. x A. y ( y e. x <-> ph ) )
7 elequ2 
 |-  ( x = z -> ( y e. x <-> y e. z ) )
8 7 imbi2d 
 |-  ( x = z -> ( ( ph -> y e. x ) <-> ( ph -> y e. z ) ) )
9 8 albidv 
 |-  ( x = z -> ( A. y ( ph -> y e. x ) <-> A. y ( ph -> y e. z ) ) )
10 9 cbvexvw 
 |-  ( E. x A. y ( ph -> y e. x ) <-> E. z A. y ( ph -> y e. z ) )
11 1 10 mpbi 
 |-  E. z A. y ( ph -> y e. z )
12 ax-sep 
 |-  E. x A. y ( y e. x <-> ( y e. z /\ ph ) )
13 11 12 exan 
 |-  E. z ( A. y ( ph -> y e. z ) /\ E. x A. y ( y e. x <-> ( y e. z /\ ph ) ) )
14 6 13 exlimiiv 
 |-  E. x A. y ( y e. x <-> ph )