I have thought about an example in set theory, but I don't know if its legal to do it, maybe someone can help. Let $\emptyset$ be given and let $A$ be a non empty set. Let us create the subset $X = \{x \in A, x \in \emptyset\}$. It appears that $X = \emptyset$, thus we have an impredicative definition $\emptyset = \{x \in A, x \in \emptyset\}$ which is quite weird.
Indeed, if $X$ is non empty, $\forall x \in X$, $x \in A \wedge x \in \emptyset$, is always false. That is, $\exists x \in X$, $x \notin A \vee x \notin \emptyset$, but if such $x$ is in $X$, then clearly $x \in A \wedge x \in \emptyset$ so the proposition is false. Hence contradiction, $X$ is non empty being false, $X$ is empty by LEM.
Note that we could have also put $X = \{ x \in \emptyset, x \notin \emptyset\}$, and we would have obtained another impredicative definition. Does set theory/FOL language allows it ? How comes it's possible ?
Your use of axioms is perfect. Set theory does allow it, one thing you cannot do is define a set using a formula in wich the set occurs in it, but that is not the case. You defined a new set $X$ and proved (via extensionality) that it is equal to the emptyset.
In fact, in the presence of axiom of infinity, axiom of empty set is unnecessary
$\emptyset = \{ x \in \omega \ | \ x \notin \omega\}$
or
$\emptyset = \{x \in \omega \ | \ x \neq x\}$