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

Metamath Proof Explorer

Theorem 2eu8

Description: Two equivalent expressions for double existential uniqueness. Curiously, we can put E! on either of the internal conjuncts but not both. We can also commute E! x E! y using 2eu7 . Usage of this theorem is discouraged because it depends on ax-13 . (Contributed by NM, 20-Feb-2005) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 2eu2 
 |-  ( E! x E. y ph -> ( E! y E! x ph <-> E! y E. x ph ) )
2 1 pm5.32i 
 |-  ( ( E! x E. y ph /\ E! y E! x ph ) <-> ( E! x E. y ph /\ E! y E. x ph ) )
3 nfeu1 
 |-  F/ x E! x ph
4 3 nfeu 
 |-  F/ x E! y E! x ph
5 4 euan 
 |-  ( E! x ( E! y E! x ph /\ E. y ph ) <-> ( E! y E! x ph /\ E! x E. y ph ) )
6 ancom 
 |-  ( ( E! x ph /\ E. y ph ) <-> ( E. y ph /\ E! x ph ) )
7 6 eubii 
 |-  ( E! y ( E! x ph /\ E. y ph ) <-> E! y ( E. y ph /\ E! x ph ) )
8 nfe1 
 |-  F/ y E. y ph
9 8 euan 
 |-  ( E! y ( E. y ph /\ E! x ph ) <-> ( E. y ph /\ E! y E! x ph ) )
10 ancom 
 |-  ( ( E. y ph /\ E! y E! x ph ) <-> ( E! y E! x ph /\ E. y ph ) )
11 7 9 10 3bitri 
 |-  ( E! y ( E! x ph /\ E. y ph ) <-> ( E! y E! x ph /\ E. y ph ) )
12 11 eubii 
 |-  ( E! x E! y ( E! x ph /\ E. y ph ) <-> E! x ( E! y E! x ph /\ E. y ph ) )
13 ancom 
 |-  ( ( E! x E. y ph /\ E! y E! x ph ) <-> ( E! y E! x ph /\ E! x E. y ph ) )
14 5 12 13 3bitr4ri 
 |-  ( ( E! x E. y ph /\ E! y E! x ph ) <-> E! x E! y ( E! x ph /\ E. y ph ) )
15 2eu7 
 |-  ( ( E! x E. y ph /\ E! y E. x ph ) <-> E! x E! y ( E. x ph /\ E. y ph ) )
16 2 14 15 3bitr3ri 
 |-  ( E! x E! y ( E. x ph /\ E. y ph ) <-> E! x E! y ( E! x ph /\ E. y ph ) )