I have the following rules for rewriting sentences with bounded quantifiers in arbitrary first-order languages to ordinary (unbounded) quantifiers:
$$\begin{align} \forall\phi(x).\psi(x)&\qquad\to\qquad\forall x.\phi(x)\implies \psi(x),\\ \exists\phi(x).\psi(x)&\qquad\to\qquad\exists x.\phi(x)\land\psi(x) \end{align}$$
... where $\phi$ and $\psi$ are formulae with free variable $x$ ($\phi$ is the scope of the quanitfier - e.g. $\forall x\in\Bbb{R}.\psi(x)$).
Additionally, I have...
$$\exists!x.\phi(x)\qquad\to\qquad \exists x.\forall y.\phi(y)\iff y=x$$
I would like to expand bounded uniqueness quantifiers in arbitrary first-order languages. (i.e. $\exists!\phi(x).\psi(x)$) in the same way as the universal and existential quantifier.
As far as I can tell, there are two ways to do this, depending on whether I apply the rule for expanding the existential or uniqueness quantifier first (provided that these rules are appropriately modified).
Applying the rule for existential quantifiers first yields the sequence of reductions:
$$\begin{align} \exists!\phi(x).\psi(x)&\qquad\to\qquad\exists!x.\phi(x)\land\psi(x)\\ &\qquad\to\qquad\exists x.\forall y.(\phi(y)\land\psi(y))\iff y=x&(\textbf{fmla 1}) \end{align}$$
Applying the rule for uniqueness quantifiers first yields:
$$\begin{align} \exists!\phi(x).\psi(x)&\qquad\to\qquad\exists\phi(x).\forall\phi(y).\psi(y)\iff y=x\\ &\qquad\to\qquad\exists \phi(x).\forall y.\phi(y)\implies(\psi(y)\iff y=x)\\ &\qquad\to\qquad\exists x.\phi(x)\land\forall y.\phi(y)\implies(\psi(y)\iff y=x)&(\textbf{fmla 2}) \end{align}$$
Analytic tableaux shows that these are nonequivalent if $=$ is taken only to be an equivalence relation.
The ncatlab page on quantifiers provides the following:
$$\exists!\, x\colon T, P(x) \;\equiv\; \exists\, x\colon T, P(x) \wedge \forall\, y\colon T, P(y) \Rightarrow (x = y)$$
...which, generalizing the typing relation to arbitrary formulae, would suggest...
$$\begin{align} \exists!\phi(x).\psi(x)&\qquad\to\qquad\exists\phi(x).\psi(x)\land\forall\phi(y).\psi(y)\implies y=x\\ &\qquad\to\qquad\exists x.\phi(x)\land\psi(x)\land\forall\phi(y).\psi(y)\implies y=x\\ &\qquad\to\qquad\exists x. \phi(x)\land\psi(x)\land\forall y.\phi(y)\implies(\psi(y)\implies y=x) & (\textbf{fmla 3}) \end{align}$$
This is most similar to formula 2, but weaker due to the replacement of the bi-implication $\psi(y)\iff y=x$ with the implication $\psi(y)\implies y=x$. Analytic tableaux shows that $\textbf{fmla 2}\implies\textbf{fmla 3}$ if $=$ is taken to be an arbitrary equivalence relationship.
Countermodels
These were obtained via analytic tableaux using the program found here (github here)
Define:
$E:=\forall x.\forall y.\forall z.R(x,x)\land(R(x,y)\implies R(y,x))\land((R(x,y)\land R(y,z))\implies R(x,z))$
(i.e. $R$ is an equivalence relation)
For $E\implies (\textbf{fmla 1}\implies\textbf{fmla 2})$ the program timed-out
$E\implies (\textbf{fmla 1}\implies\textbf{fmla 3})$ is valid
For $E\implies (\textbf{fmla 2}\implies\textbf{fmla 1})$ we have the countermodel $\mathcal{M}_1:=\langle D=\{0,1\}, R=D^2,\ \phi=\{0\},\ \psi=\{0,1\}\rangle$
$E\implies (\textbf{fmla 2}\implies \textbf{fmla 3})$ is valid
For $E\implies (\textbf{fmla 3}\implies \textbf{fmla 1})$, we have the countermodel $\mathcal{M}_2:=\langle D=\{0,1\},R=D^2,\ \phi=D,\ \psi=\{0\}\rangle$
For $E\implies (\textbf{fmla 3}\implies \textbf{fmla 2})$, we have the countermodel $\mathcal{M}_2$
The three formulations are all equivalent. The last one is the most intuitive variant and can be shortened in two steps to the first variant by essentially incorporating the $\phi$ and $\psi$ predications on $x$ into the $\forall y$ clause, by making the implication two-directional and saying that $\phi$ and $\psi$ must also hold if the object currently consiered is $x$. One may also "unsimplify" and go in the other direction from the first over the second to the third.
(1) and (2):
Transforming the biimplication into a conjunction of two implication directions:
$A \to (B \to C)$ is logically equivalent to $(A \land B) \to C$, which gives the equivalence of the $\Longrightarrow$ direction of the biimplication, $()∧() \Longrightarrow =$ and $()⟹(() \Rightarrow =)$.
The $\Longleftarrow$ direction can be obtained from (2) to (1) with $\phi(x) \land \ldots $ and $y = x$ by substituting $y$ for $x$ to obtain $\phi(y) \land \ldots $, thereby "importing" the $\psi(x)$ into the $\forall y$ clause. In the other direction from (1) to (2) one may likewise "export" and explicity specify $\phi(x)$, thereby resolving the dependency on $y = x$ and weakening the biimplication to a one-directional implication.
(2) and (3):
Analagous to above, by exporting the predication of $\psi$ on $x$ into a separate clause, the biimplication can be weakend to just the $\Rightarrow$ direction because now $\psi(x)$ is captured by an explicit predication and can do without the combination $\psi(y)$ and $y = x$.
Strenthening the implication to a biimplication with $x = y$ and substituting $y$ for $x$ makes it possible to go in the other direction and import the $\psi(x)$ into the $\forall$ clause.
(1) and (3) follows by transitivity.
I sketched these results with natural deduction proofs and was able to confirm the interderivability of all three; something must have gone wrong in your tableaus -- perhaps the treatment of the equality symbol?
Re. your counter models:
$M_1$ is not a counter model of (2) $\vDash$ (1) because it is not a model of (2) because $v(x) = 0$ is the only $x$ such that $\phi(x)$, but for $v(y) = 1$ since $\psi(y)$ but not $y = x$ the biconditional is false and hence the formula is not true for all $y$.
$M_2$ is not a counter model of (3) $\vDash$ (1) because it is a model of (1) because with $v(x) = 0$, for $v(y) = 0$, both the conjunction and the equality is true and for $v(y) = 1$, both the conjunction and the biconditional is false, and hence for all $y$ the formula is true.
$M_2$ is not a counter model of (3) $\vDash$ (2) analogously.