$\mathsf{ZF} \vdash \exists x \forall y (y\notin x)$ I'm trying to give a formal proof of $\exists x \forall y (y\notin x)$ from $\mathsf{ZF}$. I know I need to use $\mathsf{Comprehension}$ and $\mathsf{Set}$ $\mathsf{Existence}$.  I was wondering if, I could do:
\begin{align*}
&\forall z\exists x \forall y (y\in x \longleftrightarrow y\in z \land t\ne t) \text{ Comprehension with $\phi(y)=``t\ne t"$ }\\ \\
&\exists x \forall y(y\in x \longleftrightarrow y\in \tau_z \land t\ne t) \text{ Universal Instantiation} \\
& \forall y (y\in \tau_x \longleftrightarrow y\in \tau_z \land t\ne t) \text{ Existential Instantiation fixing $\tau_x$}\\
& \forall y (y\in \tau_x \longleftrightarrow y\in \tau_z \land t\ne t)\longrightarrow (\tau_y\in \tau_x \longleftrightarrow \tau_y\in \tau_z \land t\ne t) \text{ Logical Axiom}\\
& (\tau_y\in \tau_x \longleftrightarrow \tau_y\in \tau_z \land t\ne t) \text{ Modus Ponens}\\
&(\tau_y\in \tau_x \longleftrightarrow \tau_y\in \tau_z \land t\ne t)\longrightarrow (t=t\longrightarrow \tau_y\notin \tau_x) \text{ Tautology}\\
& t=t \longrightarrow \tau_y \notin \tau_x \text{ Modus Ponens}\\
&t=t \text{ Logical Axiom}\\
&\tau_y \notin \tau_x \\
&\tau_y \notin \tau_x \longrightarrow \forall y( y\notin \tau_x) \text{ Generalizing universally, as $\tau_y$ was arbitrary}\\
& \forall y(y\notin \tau_x) \text{ Modus Ponens}\\
& \forall y (y\notin \tau_x) \longrightarrow \exists x \forall y (y\notin x) \\
&\exists x \forall y (y\notin x) \text{ Modus Ponens}
\end{align*}
What do I call the second to last line? Also no where in this proof did I use set existence, did I need to ? Also, in the middle I wrote: $\tau_y \notin \tau_x \longrightarrow \forall y(y\notin \tau_x)$--I know this is wrong because $\tau_y$ is in the language. In order to generalize universally, I have to show $\mathsf{ZF} \vdash_{\mathcal{L}'=\mathcal{L}\cup \{c\}} c\notin \tau_x$. (So maybe I'd have to halt everything I did several lines up). But, on the other hand, I feel everything I did is logically valid. Any advice?
EDIT 
$\forall y (y\notin \tau_x) \longrightarrow \exists x \forall y (y\notin x)$ is Existential Generalization
 A: This is only a "long" comment, rewriting Rustyn's proof in first-order logic with equality, using the Natural Deduction proof system [see Dirk van Dalen, Logic and Structure (5th ed - 2013) ].
As per the OP's proof, we need the Axiom schema of Separation (or Specification).
From it :

$(∃x)(∀y)(y \in x \leftrightarrow (y \in a \land \varphi(y)) )$

with $\varphi(y) := y \ne y$, we have :
(1) $\mathsf {ZF} \vdash (∃x)(∀y)(y \in x \leftrightarrow (y \in a \land y \ne y) )$.
First comment
We know that at least one set exists, because in f-o logic we have $\vdash \exists x(x = x)$; the need to "validate" this principle is the "reason why" we assume in the "standard" semantics for f-o logic that the domain of interpretation must be not empty.
Having decided to develop our set theory in f-o logic, thus we have assumed that sets exist.
Having chosen the "standard" version of $\mathsf {ZF}$ without urelements (or atoms), also called "pure" set theory, we assume also that the domain contains only sets.
Thus, we have at least one set $a$ to start with in our "first application" of Separation.
end comment.
From (1), assume for $\exists$-E :
(2) $(∀y)(y \in z \leftrightarrow (y \in a \land y \ne y) )$
From (2), by $\forall$-E :
(3) $y \in z \leftrightarrow (y \in a \land y \ne y)$.
Now we use the OP's tautological implication : $\mathcal A \leftrightarrow (\mathcal B \land \mathcal C) \vDash_{TAUT} \mathcal \lnot C \rightarrow \mathcal \lnot A$, to get :
(4) $y = y \rightarrow y \notin z$.
We have $\vdash y = y$;
thus, by modus ponens :
(5) $y \notin z$
and thus, by $\forall$-I :
(6) $\forall y(y \notin z)$, because $y$ is not free in (1)
Finally, by $\exists$-I [with (1) and the auxiliary assumption (2), with $z$ not free in (7)] :
(7) $\mathsf {ZF} \vdash \exists x \forall y(y \notin x)$.
Second comment
Having proved that a set $y$ such that ... exist, we may apply Extensionality to prove that it is unique.
Thus, we may introduce a new individual constant to "name" it : $\emptyset$.
Added - May, 4th
I'll try also with an Hilbert-style proof (more "in the spirit" of the OP's proof), following Herbert Enderton, A Mathematical Introduction to Logic (2nd - 2001), which uses modus ponens as sole rule of inference.
We start assuming (2) :
$(∀y)(y \in z \leftrightarrow (y \in a \land y \ne y) )$
and we apply the logical axiom n°2 : $\forall x \alpha \rightarrow \alpha[x/t]$ [see page 112] and modus ponens to get (3) as above :
$y \in z \leftrightarrow (y \in a \land y \ne y)$.
The "tautological" step is the same; thus we have (4) :
$y = y \rightarrow y \notin z$
and by equality axiom n°5 [$y = y$, see page 112] and modus ponens we have (5) :
$y \notin z$.
Now we apply the Generalization Theorem [page 117] : If $\Gamma \vdash \varphi$ and $y$ does not occur free in any formula in $\Gamma$, then $\Gamma \vdash \forall y \varphi$. 
Thus we may conclude (6) :
$\forall y(y \notin z)$, because $y$ is not free in (2).
Up to now, we have obtained the following derivation, which makes no use of $\mathsf {ZF}$ axioms :

$(∀y)(y \in z \leftrightarrow (y \in a \land y \ne y) ) \vdash \forall y(y \notin z)$.

We apply Deduction Theorem [page 118] to get :
$\vdash (∀y)(y \in z \leftrightarrow (y \in a \land y \ne y) ) \rightarrow \forall y(y \notin z)$
and then we apply the rule of page 116 : $\alpha(x) \rightarrow \exists y \alpha(y)$ and mp to conclude :
$\vdash (\exists w) [(∀y)(y \in z \leftrightarrow (y \in a \land y \ne y) ) \rightarrow \forall y(y \notin w) ]$.
The next step needs the rule $\vdash (\alpha \rightarrow \exists w \beta) \leftrightarrow \exists w(\alpha \rightarrow \beta)$, with $w$ not free in $\alpha$ [see Exercise 8, page 130], to derive y mp :
$\vdash (∀y)(y \in z \leftrightarrow (y \in a \land y \ne y) ) \rightarrow \exists w \forall y(y \notin w)$.
Now we need the rule : if $\Gamma \vdash \alpha \rightarrow \beta$, then $\Gamma \vdash (\exists x) \alpha \rightarrow \beta$, provided that $x$ is not free in $\beta$ nor in any formula in $\Gamma$ [it is a meta-theorem provable in Enderton's system through the Generalization Th].
We apply it with $\Gamma = \emptyset$, in order to conclude :
$\vdash (\exists z)(∀y)(y \in z \leftrightarrow (y \in a \land y \ne y) ) \rightarrow \exists w \forall y(y \notin w)$.
Finally we apply mp with the Separation axiom to get (up to renaming the bound variable) :

$\mathsf {ZF} \vdash \exists x \forall y(y \notin x)$.

