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 )