As it looks like the OP has most or all of the main ideas, I'm just going to give a demonstration of what I would consider a good informal proof.
We want to prove that for any formula1 $\varphi$, there is a formula $\varphi'$ which doesn't contain any quantifiers such that $\varphi$ is logically equivalent to $\varphi'$.
We can eliminate universal quantifiers by reducing them to existential quantifiers via $\forall x.\psi(x)\iff \neg\exists x.\neg\psi(x)$. If we can handle the case $\exists x.\psi(x)$ where $\psi$ has no quantifiers, we can handle the general case by structural induction on formulas, i.e. eliminating quantifiers in a bottom-up fashion. Since $\psi(x)$ is a(n instance of a) propositional formula, we can put it into disjunctive normal form. By distribution of existential quantification over disjunction, this reduce the problem to the case where $\psi(x)$ is a conjunction of literals. Further, via $\exists x.\psi(x)\land\chi\iff(\exists x.\psi(x))\land\chi$ where $x$ does not occur in $\chi$, we can assume that $x$ occurs in all literals. The only literals are then $x=a$ and $x\neq a$ where $a$ is either a constant or a (free) variable
If $x=a$ is a literal, then we can eliminate all occurrences of $x$ by replacing them with $a$ at which point we can eliminate the quantifier via null quantification. (Except when $a$ is $x$ but then we can drop $x=x$ immediately.) The remaining case is then where all literals are of the form of $x\neq a_i$. (If one of the $a_i$ is $x$, then we can immediately reduce the conjunction to $\bot$.) Conceptually, $\psi(x)$ would then correspond to the statement that $x$ is not one of a finite set of terms, namely the $a_i$. Because the theory asserts that we have infinitely many distinct constants, $\exists x.\psi(x)$ is therefore always true2, i.e. is equivalent to $\top$ eliminating the quantifier. $\square$
If I was communicating with an expert, I would probably just say that we can reduce to a conjunction of formulas of the form $x\neq a_i$ which states that $x$ is not one of a finite set of values, but the theory asserts that there are infinitely many distinct values. All the other quantifiers can be eliminated for purely logical reasons.
1 All formulas, not just closed formulas.
2 This alludes to a semantic argument and then requires completeness if we want to show provability and not just semantic entailment. This could be improved by describing how to actually produce the formal proof. For example, how do we prove $(\exists x.x\neq y)\leftrightarrow \top$? Obviously the idea is that either $y$ is one of the constants and we can just pick any of the others, or $y$ is none of them and we can pick any constant. The problem is that we don't know which (if any) $y$ is. It isn't hard to resolve this, but it is an extra step that is needed depending on the notion of logical equivalence you're using and whether you want to assume completeness or not.