Theorem euxfr2w

Description: Transfer existential uniqueness from a variable x to another variable y contained in expression A . Version of euxfr2 with a disjoint variable condition, which does not require ax-13 . (Contributed by NM, 14-Nov-2004) Avoid ax-13 . (Revised by GG, 10-Jan-2024)

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

Proof

Step	Hyp	Ref	Expression
1		euxfr2w.1	|- A e. _V
2		euxfr2w.2	|- E* y x = A
3		2euswapv	|- ( 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		2euswapv	|- ( 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 )