Theorem euxfrw

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

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

Proof

Step	Hyp	Ref	Expression
1		euxfrw.1	|- A e. _V
2		euxfrw.2	|- E! y x = A
3		euxfrw.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	euxfr2w	|- ( E! x E. y ( x = A /\ ps ) <-> E! y ps )
14	11 13	bitri	|- ( E! x ph <-> E! y ps )