Theorem euxfr2 3391

Description: Transfer existential uniqueness from a variable x to another variable y contained in expression A. (Contributed by NM, 14-Nov-2004.)

Hypotheses

Ref	Expression
euxfr2.1	|- A e. _V
euxfr2.2	|- E* y x = A

Assertion

Ref	Expression
euxfr2	|- ( E! x E. y ( x = A /\ ph ) <-> E! y ph )

Distinct variable groups:   ph, x   x, A

Allowed substitution hints:   ph( y)   A( y)

Proof of Theorem euxfr2

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

Syntax hints:   -> wi 4   <-> wb 196   /\ wa 384   = wceq 1483   E.wex 1704   e. wcel 1990   E!weu 2470   E*wmo 2471   _Vcvv 3200

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-v 3202

This theorem is referenced by:  euxfr  3392  euop2  4974