Theorem reu3

Description: A way to express restricted uniqueness. (Contributed by NM, 24-Oct-2006)

	Ref	Expression
Assertion	reu3	$$⊢\exists !x\in A\phi \leftrightarrow \left(\exists x\in A\phi \wedge \exists y\in A\forall x\in A\left(\phi \to x=y\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		reurex	$$⊢\exists !x\in A\phi \to \exists x\in A\phi$$
2		reu6	$$⊢\exists !x\in A\phi \leftrightarrow \exists y\in A\forall x\in A\left(\phi \leftrightarrow x=y\right)$$
3		biimp	$$⊢\left(\phi \leftrightarrow x=y\right)\to \left(\phi \to x=y\right)$$
4	3	ralimi	$$⊢\forall x\in A\left(\phi \leftrightarrow x=y\right)\to \forall x\in A\left(\phi \to x=y\right)$$
5	4	reximi	$$⊢\exists y\in A\forall x\in A\left(\phi \leftrightarrow x=y\right)\to \exists y\in A\forall x\in A\left(\phi \to x=y\right)$$
6	2 5	sylbi	$$⊢\exists !x\in A\phi \to \exists y\in A\forall x\in A\left(\phi \to x=y\right)$$
7	1 6	jca	$$⊢\exists !x\in A\phi \to \left(\exists x\in A\phi \wedge \exists y\in A\forall x\in A\left(\phi \to x=y\right)\right)$$
8		rexex	$$⊢\exists y\in A\forall x\in A\left(\phi \to x=y\right)\to \exists y\forall x\in A\left(\phi \to x=y\right)$$
9	8	anim2i	$$⊢\left(\exists x\in A\phi \wedge \exists y\in A\forall x\in A\left(\phi \to x=y\right)\right)\to \left(\exists x\in A\phi \wedge \exists y\forall x\in A\left(\phi \to x=y\right)\right)$$
10		eu3v	$$⊢\exists !x\left(x\in A\wedge \phi \right)\leftrightarrow \left(\exists x\left(x\in A\wedge \phi \right)\wedge \exists y\forall x\left(\left(x\in A\wedge \phi \right)\to x=y\right)\right)$$
11		df-reu	$$⊢\exists !x\in A\phi \leftrightarrow \exists !x\left(x\in A\wedge \phi \right)$$
12		df-rex	$$⊢\exists x\in A\phi \leftrightarrow \exists x\left(x\in A\wedge \phi \right)$$
13		df-ral	$$⊢\forall x\in A\left(\phi \to x=y\right)\leftrightarrow \forall x\left(x\in A\to \left(\phi \to x=y\right)\right)$$
14		impexp	$$⊢\left(\left(x\in A\wedge \phi \right)\to x=y\right)\leftrightarrow \left(x\in A\to \left(\phi \to x=y\right)\right)$$
15	14	albii	$$⊢\forall x\left(\left(x\in A\wedge \phi \right)\to x=y\right)\leftrightarrow \forall x\left(x\in A\to \left(\phi \to x=y\right)\right)$$
16	13 15	bitr4i	$$⊢\forall x\in A\left(\phi \to x=y\right)\leftrightarrow \forall x\left(\left(x\in A\wedge \phi \right)\to x=y\right)$$
17	16	exbii	$$⊢\exists y\forall x\in A\left(\phi \to x=y\right)\leftrightarrow \exists y\forall x\left(\left(x\in A\wedge \phi \right)\to x=y\right)$$
18	12 17	anbi12i	$$⊢\left(\exists x\in A\phi \wedge \exists y\forall x\in A\left(\phi \to x=y\right)\right)\leftrightarrow \left(\exists x\left(x\in A\wedge \phi \right)\wedge \exists y\forall x\left(\left(x\in A\wedge \phi \right)\to x=y\right)\right)$$
19	10 11 18	3bitr4i	$$⊢\exists !x\in A\phi \leftrightarrow \left(\exists x\in A\phi \wedge \exists y\forall x\in A\left(\phi \to x=y\right)\right)$$
20	9 19	sylibr	$$⊢\left(\exists x\in A\phi \wedge \exists y\in A\forall x\in A\left(\phi \to x=y\right)\right)\to \exists !x\in A\phi$$
21	7 20	impbii	$$⊢\exists !x\in A\phi \leftrightarrow \left(\exists x\in A\phi \wedge \exists y\in A\forall x\in A\left(\phi \to x=y\right)\right)$$