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

Metamath Proof Explorer

Theorem euxfr2

Description: Transfer existential uniqueness from a variable x to another variable y contained in expression A . Usage of this theorem is discouraged because it depends on ax-13 . Use the weaker euxfr2w when possible. (Contributed by NM, 14-Nov-2004) (New usage is discouraged.)

Ref Expression
Hypotheses euxfr2.1 
|- A e. _V
euxfr2.2 
|- E* y x = A
Assertion euxfr2 
|- ( E! x E. y ( x = A /\ ph ) <-> E! y ph )

Proof

Step Hyp Ref Expression
1 euxfr2.1 
 |-  A e. _V
2 euxfr2.2 
 |-  E* y x = A
3 2euswap 
 |-  ( A. x E* y ( x = A /\ ph ) -> ( E! x E. y ( x = A /\ ph ) -> E! y E. x ( x = A /\ ph ) ) )
4 2 moani 
 |-  E* y ( ph /\ x = A )
5 ancom 
 |-  ( ( ph /\ x = A ) <-> ( x = A /\ ph ) )
6 5 mobii 
 |-  ( E* y ( ph /\ x = A ) <-> E* y ( x = A /\ ph ) )
7 4 6 mpbi 
 |-  E* y ( x = A /\ ph )
8 3 7 mpg 
 |-  ( E! x E. y ( x = A /\ ph ) -> E! y E. x ( x = A /\ ph ) )
9 2euswap 
 |-  ( A. y E* x ( x = A /\ ph ) -> ( E! y E. x ( x = A /\ ph ) -> E! x E. y ( x = A /\ ph ) ) )
10 moeq 
 |-  E* x x = A
11 10 moani 
 |-  E* x ( ph /\ x = A )
12 5 mobii 
 |-  ( E* x ( ph /\ x = A ) <-> E* x ( x = A /\ ph ) )
13 11 12 mpbi 
 |-  E* x ( x = A /\ ph )
14 9 13 mpg 
 |-  ( E! y E. x ( x = A /\ ph ) -> E! x E. y ( x = A /\ ph ) )
15 8 14 impbii 
 |-  ( E! x E. y ( x = A /\ ph ) <-> E! y E. x ( x = A /\ ph ) )
16 biidd 
 |-  ( x = A -> ( ph <-> ph ) )
17 1 16 ceqsexv 
 |-  ( E. x ( x = A /\ ph ) <-> ph )
18 17 eubii 
 |-  ( E! y E. x ( x = A /\ ph ) <-> E! y ph )
19 15 18 bitri 
 |-  ( E! x E. y ( x = A /\ ph ) <-> E! y ph )