Is this a proper translation of $\exists x(\emptyset \in x)$ into $\mathcal{L}_{\in}$? The symbol $\emptyset$ doesn't exist in the first-order language of set theory $\mathcal{L}_{\in}$. We can extend this language to include this symbol with this definition:
$$
\forall y(y = \emptyset \leftrightarrow \forall z(z \notin y)).
$$
Thus, we obtain the language $\mathcal{L}_{\in}[\emptyset]$. However, I am unsure how to translate a simple formula of $\mathcal{L}_{\in}[\emptyset]$, such as $\exists x(\emptyset \in x)$, into a formula of $\mathcal{L}_{\in}$. This is my attempt:
\begin{align*}
\exists x(\emptyset \in x) & \leftrightarrow \exists x \exists y(y = \emptyset \land y \in x) \\
& \leftrightarrow \exists x \exists y(\forall z(z \notin y) \land y \in x).
\end{align*}
Am I correct?
 A: Yes, that's right.
A universal quantifier could also be used (assuming we're working over a background theory strong enough to prove that there is exactly one set with no elements, which we should be if we're introducing the "$\emptyset$" symbol in the first place):
$$\exists x\forall y[\forall z(z\not\in y)\rightarrow y\in x].$$
A: Some authors may prefer the existential version for $\emptyset$, see chapter 2 of this Set Theory's language $\mathcal{L}_{\in}$. Then they use the symbol freely just as another constant in FOL, otherwise like you've experienced it's not expressive and you had to use 3 mixed quantifiers no matter the technical route to just express your statement that the (unique) empty set is a member of any set. The key idea for an expressive syntax is to leverage constant and function terms instead of relations if possible.

We let x = $\emptyset$ abbreviate ¬∃y(y $\in$ x)

This is exactly first order equivalent with your formulation per DeMorgan

let y = $\emptyset$ abbreviate $\forall z(z \notin y)$

Please note there's a subtle mistake no one pointed out for you so far regarding your above step which new logic students often make

\begin{align*}
\exists x(\emptyset \in x) & \leftrightarrow \exists x \exists y(y = \emptyset \land y \in x) \\
\end{align*}

Please note $\exists x(P(x) \land Q(x))$ is completely different from $\forall x(P(x) \rightarrow Q(x))$ semantically. Obviously here you want to express every set which is an empty set must be a member of some set $x$, thus you should proceed as:
\begin{align*}
\exists x(\emptyset \in x) & \leftrightarrow \exists x \forall y(y = \emptyset \rightarrow y \in x) ~~(1)\\
\end{align*}
Then substitute your relational definition we arrive at the same result as your previously accepted anwser:
\begin{align*}
\exists x(\emptyset \in x) & \leftrightarrow \exists x \forall y(\forall z(z \notin y) \rightarrow y \in x)  ~~(2)\\
\end{align*}
But you'd better to arrive at a prenex normal form (PNF) as follows and note that the final type of quantifier switched (see PNF reference):
\begin{align*}
\exists x(\emptyset \in x) & \leftrightarrow \exists x \forall y \exists z(z \notin y \rightarrow y \in x)  ~~(3)\\
\end{align*}
Or equivalently you can start from step (2) above via conditional replacement to arrive at:
\begin{align*}
\exists x(\emptyset \in x) & \leftrightarrow \exists x \forall y [\lnot \forall z(z \notin y) \lor y \in x] \\
\end{align*}
The per quantified DeMorgan and null quantification rules you can arrive at another prenex normal form:
\begin{align*}
\exists x(\emptyset \in x) & \leftrightarrow \exists x \forall y \exists z(z \in y \lor y \in x) ~~(4)\\
\end{align*}
