How to write a proof template to prove a uniqueness statement I must write a proof template for the uniqueness statement of the form $\exists ! x \in U, P(x)$. I thought about eliminating the uniqueness symbol and then combining other proof templates to outline a proof of the new statement. So I thought about the following 2 possible solutions:
First proof template:
I know that $\exists ! x \in U, P(x) \iff (\exists x, P(x)) \land (\forall x, \forall y, [(P(x) \land P(y)) \Rightarrow x = y])$.
Read this statement as "There exists a unique number $x$ in the infinite universe $U$" is equivalent to "There exists an $x$, such that $P(x)$ is true AND for all x and for all y, if P(x) and P(y) is true THEN x = y".
Choose $x_0$ to be a fixed number in U.
Let $x_1$ be a fixed, but arbitrary number in U.
Let $y_0$ be a fixed, but arbitrary number in U.
Proof (Direct Proof)
Assume $P(x) \land P(y)$. I must prove $x_1=y_0$.
The problem is that I am not sure if this proof template is correct or not.
Second proof template:
I also thought about writing $\exists ! x \in U, P(x)$ as $\forall x \in U, \forall y \in U, P(x) \land P(y) \Rightarrow x = y$.
Let $x_0$ be a fixed, but arbitrary number in U.
Let $y_0$ be a fixed, but arbitrary number in U.
Assume $P(x_0) \land P(y_0)$. Prove $x_0=y_0$.
Would this be a better proof template than the first one?
Concrete example using the second proof template.
Here is the exercise and how I tried to solve it:
$\exists ! x \in \mathbb{R}, 3x+5=0$.
This statement is equivalent to $\forall x \in \mathbb{R}, \forall y \in \mathbb{R}, P(x) \land P(y) \Rightarrow x = y$.
Let $x_0$ be a fixed, but arbitrary number in \mathbb{R}.
Let $y_0$ be a fixed, but arbitrary number in \mathbb{R}.
$3x_0+5=0$ so $x_0=-2$.
$3y_0+5=0$ so $y_0=-2$.
$x_0=y_0$, as needed, prooving uniqueness.
The problem that I have here is that I am not sure if I implemented it right. I know that I can't choose 2 arbitrary variables, I can't say $x_0=-2$ for example, but I don't know how to choose the values for the variables in order to show that they are equal.
 A: 
I know that $\exists ! x {\in} U\;P(x) \quad\iff\quad \exists x\;P(x) \;\land\; \forall x\;\forall y\;\big(P(x) \land P(y) \to x = y\big).\tag1$
Here is the exercise and how I tried to solve it:

$\exists ! x {\in} \mathbb{R}\;3x+5=0.$


A simpler proof is just this: $$3x+5=0\iff x=-\frac53,$$ so $\,\exists ! x {\in} \mathbb{R}\;3x+5=0.$
Alternatively, using your template $(1):$

*

*left conjunct: Put $ x=-\frac53;$ then $$3x+5=0;$$ thus, $3x+5=0$ has a real solution.

*right conjunct: For arbitrary real numbers $a$ and $b,$ $$3a+5=0\;\text{and}\;3b+5=0
    \implies a=b;$$ so, $3x+5=0$ has at most one real solution.

*Hence, $3x+5=0$ has exactly one solution.


Let $x_0$ be a fixed, but arbitrary number in $\mathbb{R}.$
Let $y_0$ be a fixed, but arbitrary number in $\mathbb{R}.$
$3x_0+5=0$ so $x_0=-2$.
$3y_0+5=0$ so $y_0=-2$.
$x_0=y_0$, as needed, proving uniqueness.
I know that I can't choose two arbitrary variables, I can't say $x_0=-2$ for example, but I don't know how to choose the values for the variables in order to show that they are equal.

You're not having to explicitly or publicly choose/pick/take/set/fix a value for $x_0,$ you're letting it be arbitrary. Specifying a value for $x_0$ prevents it from being arbitrary, since any assertion about $x_0$ is now restricted to apply only to that instantiation of $x_0.$ Relevant: 'arbitrary' versus 'any'.
