So I have a partial proof of uniqueness of the empty set in FOL:
- $\exists x \forall z(z \notin x)$ (ZF2)
- $z_1 \notin e_1 $ (Universal & Existential Instantiation of (1))
- $z_1 \notin e_2 $ (Same)
- $z_1 \in e_1 \rightarrow z_1 \in e_2$ (Tautology $\neg A \rightarrow (A \rightarrow B)$)
- $z_1 \in e_2 \rightarrow z_1 \in e_1$ (Same)
- $\forall z (z \in e_1 \rightarrow z \in e_2)$ (Uni Generalization)
- $\forall z (z \in e_2 \rightarrow z \in e_1)$ (Same)
- $\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)
- $\forall z (z \in e_1 \rightarrow z \in e_2 \land z \in e_2 \rightarrow z \in e_1)$ (Identity)
- $\forall z (z \in e_1 \leftrightarrow z \in e_2)$ (Biconditional Intro)
- $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. ), but I can't find a proof myself...