Theorem eqeu

Description: A condition which implies existential uniqueness. (Contributed by Jeff Hankins, 8-Sep-2009)

	Ref	Expression
Hypothesis	eqeu.1	$$⊢x=A\to \left(\phi \leftrightarrow \psi \right)$$
Assertion	eqeu	$$⊢\left(A\in B\wedge \psi \wedge \forall x\left(\phi \to x=A\right)\right)\to \exists !x\phi$$

Proof

Step	Hyp	Ref	Expression
1		eqeu.1	$$⊢x=A\to \left(\phi \leftrightarrow \psi \right)$$
2	1	spcegv	$$⊢A\in B\to \left(\psi \to \exists x\phi \right)$$
3	2	imp	$$⊢\left(A\in B\wedge \psi \right)\to \exists x\phi$$
4	3	3adant3	$$⊢\left(A\in B\wedge \psi \wedge \forall x\left(\phi \to x=A\right)\right)\to \exists x\phi$$
5		eqeq2	$$⊢y=A\to \left(x=y\leftrightarrow x=A\right)$$
6	5	imbi2d	$$⊢y=A\to \left(\left(\phi \to x=y\right)\leftrightarrow \left(\phi \to x=A\right)\right)$$
7	6	albidv	$$⊢y=A\to \left(\forall x\left(\phi \to x=y\right)\leftrightarrow \forall x\left(\phi \to x=A\right)\right)$$
8	7	spcegv	$$⊢A\in B\to \left(\forall x\left(\phi \to x=A\right)\to \exists y\forall x\left(\phi \to x=y\right)\right)$$
9	8	imp	$$⊢\left(A\in B\wedge \forall x\left(\phi \to x=A\right)\right)\to \exists y\forall x\left(\phi \to x=y\right)$$
10	9	3adant2	$$⊢\left(A\in B\wedge \psi \wedge \forall x\left(\phi \to x=A\right)\right)\to \exists y\forall x\left(\phi \to x=y\right)$$
11		eu3v	$$⊢\exists !x\phi \leftrightarrow \left(\exists x\phi \wedge \exists y\forall x\left(\phi \to x=y\right)\right)$$
12	4 10 11	sylanbrc	$$⊢\left(A\in B\wedge \psi \wedge \forall x\left(\phi \to x=A\right)\right)\to \exists !x\phi$$