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

Metamath Proof Explorer

Theorem 2euswap

Description: A condition allowing to swap an existential quantifier and a unique existential quantifier. Usage of this theorem is discouraged because it depends on ax-13 . Use the weaker 2euswapv when possible. (Contributed by NM, 10-Apr-2004) (New usage is discouraged.)

Ref Expression
Assertion 2euswap 
|- ( A. x E* y ph -> ( E! x E. y ph -> E! y E. x ph ) )

Proof

Step Hyp Ref Expression
1 excomim 
 |-  ( E. x E. y ph -> E. y E. x ph )
2 1 a1i 
 |-  ( A. x E* y ph -> ( E. x E. y ph -> E. y E. x ph ) )
3 2moswap 
 |-  ( A. x E* y ph -> ( E* x E. y ph -> E* y E. x ph ) )
4 2 3 anim12d 
 |-  ( A. x E* y ph -> ( ( E. x E. y ph /\ E* x E. y ph ) -> ( E. y E. x ph /\ E* y E. x ph ) ) )
5 df-eu 
 |-  ( E! x E. y ph <-> ( E. x E. y ph /\ E* x E. y ph ) )
6 df-eu 
 |-  ( E! y E. x ph <-> ( E. y E. x ph /\ E* y E. x ph ) )
7 4 5 6 3imtr4g 
 |-  ( A. x E* y ph -> ( E! x E. y ph -> E! y E. x ph ) )