How To prove the logical equivalence for uniqueness quantifier Could you please help me out with this little issue, I need to know how to prove the following assertion. I'll be very thankful for your efforts :) 
Thanks in advance,
$$\exists !xP(x) \equiv \exists x(P(x) \land \forall y(P(y) \rightarrow y=x))$$
 A: $$\exists !xP(x) \equiv \exists x(P(x) \land \forall y(P(y) \rightarrow y=x))$$
The right hand side of the equivalence is taken to be the definition of uniqueness operator, where $P(x)$ is any predicate about $x$.
Both sides of the equivalence can be translated to
"There exists a unique $x$ such that $P(x)$" $\;\equiv \;\;$"There exists one and only one $x$ such that $P(x)$".
The right hand side simply defines what it means to assert the existence of one and only one $x$ such that $P(x)$:
$(1)$ there exists $x$ such that $P(x)$ (existence of $x$ for which $P(x)$)
and that
$(2)$ for any $y$, if $P(y)$ is true, then $y$ must be (must equal) $x$ (uniqueness of $x$ such that $P(x)$).

A: I'm no expert at this but, I'm giving this a shot.
$\exists !xP(x)$
$\equiv$ There exists x such that $P(x)$ and No other $x$ exists such that $P(x)$
$\equiv \exists x P(x) \land $ No other $x$ exists such that $P(x)$
$\equiv \exists x P(x) \land \lnot$ (There exists other $x$ such that $P(x))$
$\equiv \exists x P(x) \land \lnot$ (There exists $y$ such that $P(y) \land x \neq y)$
$\equiv \exists x P(x) \land \lnot (\exists y P(y) \land x \neq y)$
$\equiv \exists x P(x) \land (\forall y \lnot P(y) \lor x = y)$
$\equiv \exists x P(x) \land \forall y( \lnot P(y) \lor x = y)$
$\equiv \exists x ( P(x) \land \forall y( \lnot P(y) \lor x = y))$
