$\exists! x:Px\implies (\forall x(Px \implies Qx) \iff \exists x(Px \land Qx))$
Essentially, the values of x for which P is true form partitions of the universe. This question came to mind when considering the definition of the absolute value of real numbers:
$abs=\{ (x,y)|(x>0 \implies y=x) \land (x\le 0 \implies y=-x)\}$
Which is actually equivalent to:
$abs=\{ (x,y)|x>0 \land y=x \lor x\le 0 \land y=-x\}$
In this case we have only 2 partitions, $\{ x|x>0\}$ and $\{x|x\le 0\}$. I am able to prove the equivalency of the two definitions of the absolute value function using rules from propositional logic, but I have difficulty when facing 3, 4 or more partitions, hence why I am asking here.
Assume $\exists!x\colon Px$.
So let $x_0$ with $Px_0$ and $\forall x\colon Px\to x=x_0$.
Assume $\forall x(Px\to Qx)$. By specialization, $Px_0\to Qx_0$. By modus ponens, $Qx_0$. As also $Px_0$, we have $Px_0\land Qx_0$, hence $\exists x(Px\land Qx)$. This proves $$ \forall x(Px\to Qx)\to\exists x(Px\land Qx) .$$
Next, assume $\exists x(Px\land Qx)$ and let $x_1$ with $Px_1\land Qx_1$. In particular, $Px_1$. Specialize $\forall x\colon Px\to x=x_0$ to $Px_1\to x_1=x_0$, and so by modus ponens $x_1=x_0$. Also $Qx_1$, hence from $x_1=x_0$ also $Qx_0$. In order to show $\forall x(Px\to Qx)$, let $x$ be arbitrary and assume $Px$. Then again $x=x_0$, and so from $Qx_0$ also $Qx$. This shows $Px\to Qx$, and as $x$ was arbitrary, $\forall x(Px\to Qx)$. In summary, this proves $$ \exists x(Px\land Qx)\to \forall x(Px\to Qx).$$
Combined, we have proved $$ \forall x(Px\to Qx)\leftrightarrow\exists x(Px\land Qx) $$ under the assumption $\exists!x\colon Px$, so we can discharge one last time to
$$\exists!x\colon Px \to (\forall x(Px\to Qx)\leftrightarrow\exists x(Px\land Qx)). $$