Definitions of exists unique 
$\exists!x_0 \in S,P(x_0)$
Definitions:
1.$\exists x_0 \in S, P(x_0)\wedge(\forall x_1,x_2 \in S, P(x_1)\wedge P(x_2)\rightarrow x_1=x_2)$
2.$\exists x_0 \in S, P(x_0)\wedge (\forall x_1 \in S,P(x_1)\rightarrow x_0=x_1)$
$3. \exists x_0 \in S, \ \forall x_1 \in S, (P(x_1) \leftrightarrow x_0 = x_1))$


Question: I saw people sometimes use first one and sometimes use the second one in uniqueness proofs, are they equivalent, if so, is it possible to prove it?
 A: Yes, they are equivalent:
Obviously the first part is the same in both definitions so let $x_0$ with $P(x_0)$ be given. Now
$1. \Rightarrow 2.$, by setting $x_2=x_0$ in "$1.$".
To see "$2. \Rightarrow 1.$", given $x_1, x_2$ you can see that $x_0=x_1$ and $x_0=x_2$ by "$2.$" and thus $x_1=x_2$.
A: Passing from (1) to (2) is trivial, it suffices to let $x_2=x_0$. Now we will start with assuming (2) as true. We have
$$\forall x_1,x_2 \in S \big( P(x_1) \land P(x_2) \Rightarrow x_0=x_1 \land x_0=x_2\big)$$which leads to$$\forall x_1,x_2 \in S \big( P(x_1) \land P(x_2) \Rightarrow x_1=x_2\big)$$and we have just demonstrated (1).
A: Yes, they are equivalent. In fact, here is a third one that is equivalent:
$3. \exists x_0 \in S \ \forall x_1 \in S (P(x1) \leftrightarrow x_0 = x_1))$
To prove these three are all equivalent, let's show $1 \Rightarrow 2$, $2 \Rightarrow 3$, and $3 \Rightarrow 1$. I'll use the Fitch proof system. Please note that this system does not allow me to specify restricted domains, but that changes nothing:
First, $1 \Rightarrow 2$:

Then, $2 \Rightarrow 3$:

Finally, $3 \Rightarrow 1$:

