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

Metamath Proof Explorer

Theorem 2eu2

Description: Double existential uniqueness. Usage of this theorem is discouraged because it depends on ax-13 . (Contributed by NM, 3-Dec-2001) (New usage is discouraged.)

Ref Expression
Assertion 2eu2 
|- ( E! y E. x ph -> ( E! x E! y ph <-> E! x E. y ph ) )

Proof

Step Hyp Ref Expression
1 eumo 
 |-  ( E! y E. x ph -> E* y E. x ph )
2 2moex 
 |-  ( E* y E. x ph -> A. x E* y ph )
3 2eu1 
 |-  ( A. x E* y ph -> ( E! x E! y ph <-> ( E! x E. y ph /\ E! y E. x ph ) ) )
4 simpl 
 |-  ( ( E! x E. y ph /\ E! y E. x ph ) -> E! x E. y ph )
5 3 4 biimtrdi 
 |-  ( A. x E* y ph -> ( E! x E! y ph -> E! x E. y ph ) )
6 1 2 5 3syl 
 |-  ( E! y E. x ph -> ( E! x E! y ph -> E! x E. y ph ) )
7 2exeu 
 |-  ( ( E! x E. y ph /\ E! y E. x ph ) -> E! x E! y ph )
8 7 expcom 
 |-  ( E! y E. x ph -> ( E! x E. y ph -> E! x E! y ph ) )
9 6 8 impbid 
 |-  ( E! y E. x ph -> ( E! x E! y ph <-> E! x E. y ph ) )