By formal proof I mean a finite sequence of strings in the language of ZFC that begins with a subset of the axioms of ZFC and ends with the sentence $\exists x.\forall y.(\forall z.\neg(z\in y)\iff (x=y))$, such that each string is either an axiom or a theorem provable from the axioms and inference rules of FOL – e.g. Hilbert proof, natural deduction, etc. [see edit]. Specifically, I am looking for a proof in the language of ZFC proper, without extending it by the constant symbol "$\emptyset$" (this is why I need to ask – the proof is trivial, otherwise).
I've looked through a couple of repositories for theorem provers, but even these seem to rely on introducing a new symbol to express the empty set.
I assume that the proof exists somewhere, probably in some dusty preprint from 1913, but I haven't been able to find it yet.
Note/Response to comments: I do not doubt the uniqueness of the empty set, nor am I asking for an explanation of the intuition behind a proof of the uniqueness of the empty set. I understand that the axiom of extensionality implies the uniqueness of the empty set. This question is strictly about the formal proof of uniqueness – i.e. which inference rules and axioms must be used and in what order to conclude the uniqueness of the empty set – specifically in the language whose only non-logical symbol is $\in$. To be absolutely, 200% clear, this will, at some point, be read by a machine. Said machine is only intended to recognize the following symbols: $\forall,\exists,\land,\lor,\neg,\implies,\iff,=,(,),.,',\in, x$, and nothing else.
Now, I could brute-force it by systematically applying every inference rule to every axiom, adding the result to the set of axioms and repeating until I get the desired theorem, but 1) that could take days of nonstop running and 2) I really don't want to do that, especially if someone else already did it 100 years ago.
Edit: As it turns out, natural deduction systems [particularly Fitch-style?] and their kin have something that Hilbert systems do not: the ability to introduce new variables through existential instantiation, like so…
$$\dfrac{\exists x.\phi}{\phi(\alpha/ x)}\exists E$$
…provided that $\alpha$ does not occur free in any previous lines.
According to this, these are known as Skolem terms, and they act as "virtual" constants in a proof. This would be used, for instance, in the formalization of the proof sketch in Alex Kruckman's answer (i.e. "let $x$ be such a set"). While these terms cannot appear in the conclusion of a proof, they can appear in premises or "subproofs." This violates the condition that every sentence of the proof be either an axiom or a theorem. Despite its being fundamental to mathematical logic, I was not aware of this detail until yesterday (it wasn't especially relevant until a few days ago).
Best Answer
I think you already know the proof! But I'll write it here in great detail so that the logical structure is clear:
By the empty set axiom, there exists a set with no elements. Let $x$ be such a set. Now let $y$ be an arbitrary set. If $x=y$, then $y$ has no elements. Conversely, if $y$ has no elements, then $x$ and $y$ have the same elements. By the extensionality axiom, $x=y$. Thus, there exists $x$ such that for any $y$, $y$ has no elements if and only if $x=y$.
What remains is an exercise in formalization: translating the above proof into a formal proof. This can, of course, be done - the argument above is relatively simple first-order reasoning, which is fairly straightforward to implement in any standard proof system. But the details will depend on your choice of proof system and specific formulation of the axioms of empty set and extensionality.
Edit: Based on the latest edit to your question and your concern about proofs which introduce a new symbol for the empty set, it seems you're especially caught up on the step of the proof where I say "Let $x$ be such a set" (a set with no elements).
It's a fundamental feature of first-order reasoning that if we can prove an existential statement, then we can name a witness by a variable and use it in further reasoning. In informal proofs, this is often realized by the ubiquitous phrase "Let $x$ be ..." In formal proofs systems, this form of reasoning is implemented in various ways, but it is always present.
The "$\exists E$" rule in your post is one such implementation. I share your distaste for proof systems containing the rule in this form, but this is not the only way to go, even in natural deduction systems - see my comments here.
In a Hilbert system, we would instead have $\exists x \varphi\rightarrow ((\forall x(\varphi\rightarrow \psi))\rightarrow \psi)$, where $x$ does not occur free in $\psi$. Depending on how your Hilbert system handles quantifiers, this might be an axiom or just derivable - see the posted I linked to in the previous paragraph for a derivation in one particular Hilbert system. But the point is that it captures the same pattern of reasoning discussed above: Suppose we can prove $\exists x\varphi$. Now assume $\varphi$ (and note that $x$ is now a free variable naming the witness to the quantifier) and prove $\psi$ in which $x$ is not free. By the deduction theorem, $(\varphi\rightarrow \psi)$, and by generalization $\forall x(\varphi\rightarrow \psi)$. By our axiom and modus ponens twice, we have $\psi$.
Edit 2: Below, I've written a natural deduction proof of the uniqueness of the empty set. If anything is not clear, let me know.
\begin{align*} (1) &\quad \exists x \forall z (\lnot z\in x) &\quad (\textbf{Empty set})\\ (2) &\quad\quad \forall z(\lnot z\in x) & \quad (\text{Assumption})\\ (3) &\quad\quad\quad x = y & \quad (\text{Assumption})\\ (4) &\quad\quad\quad \forall z(\lnot z\in y) & \quad (= E: 2, 3)\\ (5) &\quad\quad (x = y)\rightarrow \forall z(\lnot z\in y) & \quad (\rightarrow I: 3-4)\\ (6) &\quad\quad\quad \forall z(\lnot z\in y) &\quad (\text{Assumption})\\ (7) & \quad\quad\quad \lnot z\in y &\quad (\forall E: 6)\\ (8) &\quad\quad\quad\quad z\in y &\quad (\text{Assumption})\\ (9) &\quad \quad\quad\quad z\in x &\quad (\lnot E: 7,8)\\ (10) &\quad\quad\quad (z\in y)\rightarrow (z\in x) &\quad (\rightarrow I: 8-9)\\ (11) & \quad\quad\quad \lnot z\in x &\quad (\forall E: 2)\\ (12) &\quad\quad\quad\quad z\in x &\quad (\text{Assumption})\\ (13) &\quad \quad\quad\quad z\in y &\quad (\lnot E: 11,12)\\ (14) &\quad\quad\quad (z\in x)\rightarrow (z\in y) &\quad (\rightarrow I: 12-13)\\ (15) &\quad\quad\quad (z\in x)\leftrightarrow (z\in y) &\quad (\leftrightarrow I: 10, 14)\\ (16) &\quad\quad\quad \forall z( (z\in x)\leftrightarrow (z\in y)) &\quad (\forall I: 15)\\ (17) &\quad\quad\quad \forall x\forall y(\forall z( (z\in x)\leftrightarrow (z\in y))\rightarrow (x=y))& \quad(\textbf{Extensionality})\\ (18) &\quad\quad\quad \forall y(\forall z( (z\in x)\leftrightarrow (z\in y))\rightarrow (x=y))& \quad(\forall E: 15)\\ (19) &\quad\quad\quad \forall z( (z\in x)\leftrightarrow (z\in y))\rightarrow (x=y)& \quad(\forall E: 16)\\ (20) & \quad\quad\quad x = y & \quad (\rightarrow E: 16, 19)\\ (21) & \quad\quad \forall z (\lnot z\in y)\rightarrow (x = y) &\quad (\rightarrow I: 6-20)\\ (22) & \quad\quad \forall z(\lnot z\in y)\leftrightarrow (x=y) &\quad (\leftrightarrow I: 5, 21)\\ (23) & \quad\quad \forall y(\forall z(\lnot z\in y)\leftrightarrow (x=y)) &\quad (\forall I: 22)\\ (24) & \quad\quad \exists x\forall y(\forall z(\lnot z\in y)\leftrightarrow (x=y)) &\quad (\exists I: 23)\\ (25) & \quad \exists x\forall y(\forall z(\lnot z\in y)\leftrightarrow (x=y)) &\quad (\exists E: 1, 2-24)\\ \end{align*}