Theorem euxfr

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 euxfrw when possible. (Contributed by NM, 14-Nov-2004) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		euxfr.1	$$⊢A\in \mathrm{V}$$
2		euxfr.2	$$⊢\exists !yx=A$$
3		euxfr.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	euxfr2	$$⊢\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$$