Theorem moxfr

Description: Transfer at-most-one between related expressions. (Contributed by Stefan O'Rear, 12-Feb-2015)

	Ref	Expression
Hypotheses	moxfr.a	$$⊢A\in \mathrm{V}$$
	moxfr.b	$$⊢\exists !yx=A$$
	moxfr.c	$$⊢x=A\to \left(\phi \leftrightarrow \psi \right)$$
Assertion	moxfr	$$⊢{\exists }^{*}x\phi \leftrightarrow {\exists }^{*}y\psi$$

Proof

Step	Hyp	Ref	Expression
1		moxfr.a	$$⊢A\in \mathrm{V}$$
2		moxfr.b	$$⊢\exists !yx=A$$
3		moxfr.c	$$⊢x=A\to \left(\phi \leftrightarrow \psi \right)$$
4	1	a1i	$$⊢y\in \mathrm{V}\to A\in \mathrm{V}$$
5		euex	$$⊢\exists !yx=A\to \exists yx=A$$
6	2 5	ax-mp	$$⊢\exists yx=A$$
7		rexv	$$⊢\exists y\in \mathrm{V}x=A\leftrightarrow \exists yx=A$$
8	6 7	mpbir	$$⊢\exists y\in \mathrm{V}x=A$$
9	8	a1i	$$⊢x\in \mathrm{V}\to \exists y\in \mathrm{V}x=A$$
10	4 9 3	rexxfr	$$⊢\exists x\in \mathrm{V}\phi \leftrightarrow \exists y\in \mathrm{V}\psi$$
11		rexv	$$⊢\exists x\in \mathrm{V}\phi \leftrightarrow \exists x\phi$$
12		rexv	$$⊢\exists y\in \mathrm{V}\psi \leftrightarrow \exists y\psi$$
13	10 11 12	3bitr3i	$$⊢\exists x\phi \leftrightarrow \exists y\psi$$
14	1 2 3	euxfrw	$$⊢\exists !x\phi \leftrightarrow \exists !y\psi$$
15	13 14	imbi12i	$$⊢\left(\exists x\phi \to \exists !x\phi \right)\leftrightarrow \left(\exists y\psi \to \exists !y\psi \right)$$
16		moeu	$$⊢{\exists }^{*}x\phi \leftrightarrow \left(\exists x\phi \to \exists !x\phi \right)$$
17		moeu	$$⊢{\exists }^{*}y\psi \leftrightarrow \left(\exists y\psi \to \exists !y\psi \right)$$
18	15 16 17	3bitr4i	$$⊢{\exists }^{*}x\phi \leftrightarrow {\exists }^{*}y\psi$$