We are trying to prove $\models \forall x\exists x.x=x \to \exists x.x=x$, i.e., for all structures $\mathfrak{A}$, if $\mathfrak{A} \models \forall x\exists x.x=x$, then $\mathfrak{A} \models \exists x.x=x$. We proceed with the definition of $\models$. $A$ is the domain of $\mathfrak{A}$, $\forall^M$ and $\exists^M$ are metalogical quantifiers (equivalent to writing $\text{for all}$ and $\text{there exists}$ in English) and $x \mapsto a$ denotes the value of $x$ for some assignment function $\sigma$, where the $\sigma + (y \mapsto b)$ means changing $\sigma(y)$ to $b$. In what follows, $\Leftrightarrow$ and $\Rightarrow$ are the metalogical equivalence and implication.
\begin{align*} &\mathfrak{A} \models \forall x\exists x.x=x \\ &\Leftrightarrow \forall^M a \in A.\mathfrak{A} \models \exists x.x=x[(x\mapsto a)] \\ &\Leftrightarrow \forall^M a \in A \exists^Mb \in A.\mathfrak{A} \models x=x[(x\mapsto a) + (x \mapsto b)] \\ &\Leftrightarrow \forall^M a \in A \exists^Mb \in A.\mathfrak{A} \models x=x[(x \mapsto b)] \\ &\Leftrightarrow \forall^M a \in A.\mathfrak{A} \models \exists x. x=x \\ &\Leftrightarrow \mathfrak{A} \models \exists x. x=x. \end{align*}
Indeed, with this, we have proved even $\models \forall x\exists x.x=x \leftrightarrow \exists x.x=x$. In line 3, the definition overrides $\sigma$ at $x$, so in line 4, $\forall^M a$ doesn't bind anything anymore. Now, the crucial step is going from line 5 to line 6. I reasoned that, since $\forall^M a$ does not bind anything, the metalogical formula which drops it is equivalent to the previous one. But this seems dubious to me, because it is purely intuitive and informal. One attempt at making this formal would be:
\begin{align*} &\forall^M a \in A.\mathfrak{A} \models \exists x. x=x \\ &\Leftrightarrow \forall^M a.( a \in A \Rightarrow \mathfrak{A} \models \exists x. x=x) \\ &\Leftrightarrow \exists^M a.a \in A \Rightarrow \mathfrak{A} \models \exists x. x=x \\ &\Leftrightarrow \mathfrak{A} \models \exists x. x=x. \end{align*}
The second equivalence is justified by the fact that $a$ does not occur free in $\mathfrak{A} \models \exists x. x=x$. The third equivalence is justified by the fact that classical model theory requires domains to be non-empty. But still, I feel like this is circular. For the second equivalence, I used a well-known result from FOL, which itself needs model theory in the first place to confirm it as true.
If anyone knows how to deal rigorously with this situation without raising my worries, please do tell. Thank you!