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)$.
