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

Metamath Proof Explorer

Theorem euxfr

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 euxfrw when possible. (Contributed by NM, 14-Nov-2004) (New usage is discouraged.)

Ref Expression
Hypotheses euxfr.1 
|- A e. _V
euxfr.2 
|- E! y x = A
euxfr.3 
|- ( x = A -> ( ph <-> ps ) )
Assertion euxfr 
|- ( E! x ph <-> E! y ps )

Proof

Step Hyp Ref Expression
1 euxfr.1 
 |-  A e. _V
2 euxfr.2 
 |-  E! y x = A
3 euxfr.3 
 |-  ( x = A -> ( ph <-> ps ) )
4 euex 
 |-  ( E! y x = A -> E. y x = A )
5 2 4 ax-mp 
 |-  E. y x = A
6 5 biantrur 
 |-  ( ph <-> ( E. y x = A /\ ph ) )
7 19.41v 
 |-  ( E. y ( x = A /\ ph ) <-> ( E. y x = A /\ ph ) )
8 3 pm5.32i 
 |-  ( ( x = A /\ ph ) <-> ( x = A /\ ps ) )
9 8 exbii 
 |-  ( E. y ( x = A /\ ph ) <-> E. y ( x = A /\ ps ) )
10 6 7 9 3bitr2i 
 |-  ( ph <-> E. y ( x = A /\ ps ) )
11 10 eubii 
 |-  ( E! x ph <-> E! x E. y ( x = A /\ ps ) )
12 2 eumoi 
 |-  E* y x = A
13 1 12 euxfr2 
 |-  ( E! x E. y ( x = A /\ ps ) <-> E! y ps )
14 11 13 bitri 
 |-  ( E! x ph <-> E! y ps )