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

Metamath Proof Explorer

Theorem 2eu7

Description: Two equivalent expressions for double existential uniqueness. Usage of this theorem is discouraged because it depends on ax-13 . (Contributed by NM, 19-Feb-2005) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 nfe1 
 |-  F/ x E. x ph
2 1 nfeu 
 |-  F/ x E! y E. x ph
3 2 euan 
 |-  ( E! x ( E! y E. x ph /\ E. y ph ) <-> ( E! y E. x ph /\ E! x E. y ph ) )
4 ancom 
 |-  ( ( E. x ph /\ E. y ph ) <-> ( E. y ph /\ E. x ph ) )
5 4 eubii 
 |-  ( E! y ( E. x ph /\ E. y ph ) <-> E! y ( E. y ph /\ E. x ph ) )
6 nfe1 
 |-  F/ y E. y ph
7 6 euan 
 |-  ( E! y ( E. y ph /\ E. x ph ) <-> ( E. y ph /\ E! y E. x ph ) )
8 ancom 
 |-  ( ( E. y ph /\ E! y E. x ph ) <-> ( E! y E. x ph /\ E. y ph ) )
9 5 7 8 3bitri 
 |-  ( E! y ( E. x ph /\ E. y ph ) <-> ( E! y E. x ph /\ E. y ph ) )
10 9 eubii 
 |-  ( E! x E! y ( E. x ph /\ E. y ph ) <-> E! x ( E! y E. x ph /\ E. y ph ) )
11 ancom 
 |-  ( ( E! x E. y ph /\ E! y E. x ph ) <-> ( E! y E. x ph /\ E! x E. y ph ) )
12 3 10 11 3bitr4ri 
 |-  ( ( E! x E. y ph /\ E! y E. x ph ) <-> E! x E! y ( E. x ph /\ E. y ph ) )