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) Avoid ax-13 . (Revised by Gino Giotto, 10-Jan-2024)

	Ref	Expression
Hypotheses	euxfrw.1	$$⊢A\in \mathrm{V}$$
	euxfrw.2	$$⊢\exists !yx=A$$
	euxfrw.3	$$⊢x=A\to \left(\phi \leftrightarrow \psi \right)$$
Assertion	euxfrw	$$⊢\exists !x\phi \leftrightarrow \exists !y\psi$$

Proof

Step	Hyp	Ref	Expression
1		euxfrw.1	$$⊢A\in \mathrm{V}$$
2		euxfrw.2	$$⊢\exists !yx=A$$
3		euxfrw.3	$$⊢x=A\to \left(\phi \leftrightarrow \psi \right)$$
4		euex	$$⊢\exists !yx=A\to \exists yx=A$$
5	2 4	ax-mp	$$⊢\exists yx=A$$
6	5	biantrur	$$⊢\phi \leftrightarrow \left(\exists yx=A\wedge \phi \right)$$
7		19.41v	$$⊢\exists y\left(x=A\wedge \phi \right)\leftrightarrow \left(\exists yx=A\wedge \phi \right)$$
8	3	pm5.32i	$$⊢\left(x=A\wedge \phi \right)\leftrightarrow \left(x=A\wedge \psi \right)$$
9	8	exbii	$$⊢\exists y\left(x=A\wedge \phi \right)\leftrightarrow \exists y\left(x=A\wedge \psi \right)$$
10	6 7 9	3bitr2i	$$⊢\phi \leftrightarrow \exists y\left(x=A\wedge \psi \right)$$
11	10	eubii	$$⊢\exists !x\phi \leftrightarrow \exists !x\exists y\left(x=A\wedge \psi \right)$$
12	2	eumoi	$$⊢{\exists }^{*}yx=A$$
13	1 12	euxfr2w	$$⊢\exists !x\exists y\left(x=A\wedge \psi \right)\leftrightarrow \exists !y\psi$$
14	11 13	bitri	$$⊢\exists !x\phi \leftrightarrow \exists !y\psi$$