I am wondering how one would go about this. I am using Hilbert style proof system as described in Kleene's "Introduction to Metamathematics" or "Mathematical logic". I am pretty sure that if you can give the proof in your preferred system then I will be able to translate it (hopefully). I am using predicate calculus with equality. Also, I hope that it is clear from the context which symbol is variable, term, formula, held free, held fixed, and so forth. If not, please let me know. $\exists !x (A(x))$ stands for $\exists x (A(x) \land \forall y (A(y) \implies y=x))$.
- $ \lnot \exists x (t=x \land \forall y (t=y \implies y=x)) \vdash \forall x(\lnot(t=x \land \forall y (t=y \implies y=x))) \vdash \lnot(t=t \land \forall y (t=y \implies y=t))$.
By negation of existential quantifier and by $\forall$- elimination where $t$ is free for $x$.
- $\vdash t=t$.
Axiom for equality.
- $\vdash t = y \implies y = t$, so $\vdash \forall y(t=y \implies y=t)$.
By property of equality and $\forall$-introduction where $y$ is free for $y$.
Combining three results we obtain a contradiction, so, by skipping some steps,
- $\vdash \lnot \lnot \exists x (t=x \land \forall y (t=y \implies y=x)) \vdash \exists x (t=x \land \forall y (t=y \implies y=x))$
By $\lnot$-introduction and $\lnot$-elimination.