Is it possible to prove empty set uniqueness in FOL directly (without proof by contradiction)

Question

So I have a partial proof of uniqueness of the empty set in FOL:

1. $\exists x \forall z(z \notin x)$ (ZF2)
2. $z_1 \notin e_1 $ (Universal & Existential Instantiation of (1))
3. $z_1 \notin e_2 $ (Same)
4. $z_1 \in e_1 \rightarrow z_1 \in e_2$ (Tautology $\neg A \rightarrow (A \rightarrow B)$)
5. $z_1 \in e_2 \rightarrow z_1 \in e_1$ (Same)
6. $\forall z (z \in e_1 \rightarrow z \in e_2)$ (Uni Generalization)
7. $\forall z (z \in e_2 \rightarrow z \in e_1)$ (Same)
8. $\forall z (z \in e_1 \rightarrow z \in e_2) \land \forall z (z \in e_2 \rightarrow z \in e_1)$ (Conj Intro)
9. $\forall z (z \in e_1 \rightarrow z \in e_2 \land z \in e_2 \rightarrow z \in e_1)$ (Identity)
10. $\forall z (z \in e_1 \leftrightarrow z \in e_2)$ (Biconditional Intro)
11. $e_1 = e_2$ (Eq Intro)

So far, so good. But what I actually want to prove is: $$\forall x \forall y [(\forall z (z \notin x) \land \forall z (z \notin y)) \rightarrow x = y] .....P$$

As hard as I try, I can't go from (1)-(11) to $P$.

Basically where I'm struggling is turning the $e$'s into $\forall$ statements. Since $e$'s are constants, we can only do existential generalization, not universal generalization. I guess my question boils down to whether there is some theorem that allows us to go from constants/existential quantifiers to universal ones. My suspect is "$(\exists x P(x))\rightarrow Q$ is equivalent to $\forall x (P \rightarrow Q)$ (as long as $x$ is not in $Q$)", but I can't seem to put the pieces together in the right way. ;)

Everyone seems to agree that it is possible to prove empty set uniqueness directly (e.g. [1]), but I can't find a proof myself...

Answer 1

I think I got it!

I'm going to write a bunch of implications and then join the first and last:

$\quad \forall z (z \notin x) \land \forall z (z \notin y)$

$\rightarrow \forall z (z \notin x), \forall z (z \notin y)$ (Conj Elim)

$\rightarrow z \notin x, z \notin y$ (Univ Inst)

$\rightarrow z \in x \rightarrow z \in y, z \in y \rightarrow z \in x$ (Tautology $\neg A \rightarrow (A \rightarrow B))$

$\rightarrow z \in x \rightarrow z \in y \land z \in y \rightarrow z \in x$ (Conj Intro)

$\rightarrow \forall z (z \in x \rightarrow z \in y \land z \in y \rightarrow z \in x)$ (Univ Gen)

$\rightarrow \forall z(z\in x \leftrightarrow z\in y)$ (Biconditional Intro)

$\rightarrow x=y$ (Eq Intro/Axiom of Ext)

Hence:

$$(\forall z (z \notin x) \land \forall z (z \notin y)) \rightarrow x=y$$

So, by universal generalization

$$\forall x \forall y [(\forall z (z \notin x) \land \forall z (z \notin y)) \rightarrow x=y]$$