Prove that: $$\vdash \forall x \exists !y(y=x)$$ in first order logic.
The first thing to do would be to write this as $$\forall x (\exists y(y=x) \land \forall y\forall z (y=x \land z=x \to y=z))$$
However, I cannot proceed from here. The equality axioms of first order theories don't seem to give me anything.
On
That was tricky! This isn't standard FOL, but you should be able to translate it if you are familiar with all the "subtleties" of standard FOL (I am not). I introduce the unary predicate $U$ to make the domain of discussion explicit. (This is not the usual practice in standard FOL.) Using this convention, we want to prove:
$$\forall x:[U(x) \implies \exists y:[U(y) \land [x=y \land \forall z:[U(z)\implies [x=z \implies y=z]]]]]$$
Proof:
$U(a)$ (Premise)
$a=a$ (Reflexivity)
$U(c)$ (Premise)
$a=c$ (Premise)
$a=c \implies a=c$ (Conclusion, 4)
$\forall z:[U(z) \implies [a=z \implies a=z]]$ (Conclusion, 3)
$a=a \land \forall z:[U(z) \implies [a=z \implies a=z]]$ (Join, 2,6)
$U(a) \land [a=a \land \forall z:[U(z) \implies [a=z \implies a=z]]]$ (Join, 1, 7)
$\exists y:[U(y) \land [a=y \land \forall z:[U(z) \implies [a=z \implies y=z]]]$ (E Gen, 8)
$\forall x:[U(x) \implies \exists y:[U(y) \land [x=y \land \forall z:[U(z)\implies [x=z \implies y=z]]]]]$ (Conclusion, 1)
This seems like a formal matter, thus I will describe how you do this formally using proof rules.
In order to prove $$\forall x (\exists y(y=x) \land \forall y\forall z (y=x \land z=x \to y=z))$$ We show that $$\exists y(y=a) \land \forall y\forall z (y=a \land z=a \to y=z))$$ hold for a general constant $a$, and then if we want to be formal use $\forall$-introduction.
To prove $\exists y(y=a)$ we may just notice that $a=a$ hold by $=-$introduction and then use $\exists$-intrudction to prove $\exists y(y=a)$. If we want to use the axioms for equality instead of the $=-$introduction rule, we may use $\forall x(x=x)$ and use $\forall-$elimination to conclude that $a=a$ hold and then continue as above.
In order to prove $\forall y\forall z (y=a \land z=a \to y=z))$ We assume that $b,c$ are general constants such that $b=a\land c=a$ hold. Now we may use $=$-elimination (or equality axioms) to conclude that $b=c$ hold. If we want to use the axioms for equality instead we may use the axiom $\forall x\forall y (y=x \wedge P(x)\rightarrow P(y))$, which should hold for any predicate $P$ Thus it also hold if P is the predicate $c=x$. In this case we get the formula $$\forall x\forall y (y=x \wedge x=c\rightarrow y=c)$$ If we do $\forall-$eliminationputting in $a$ and $c$ we get $a=b\wedge b=c\rightarrow a = c$. which we may use to prove what we wanted.
To finnish the proof we use $\forall-introduction to conclude the formla we want to prove.