Definitions of exists unique

Question

$\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?

Answer 1

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$:

Answer 2

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$.

Answer 3

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).