I am trying to understand natural deduction in first order logic, but am confused about the $\forall$ and $\exists$ elimination rules.
My understanding:
If we know $\forall x \phi$ then we can substitute all free occurrences of $x$ in $\phi$ with a term $x_0$ because irrespective of the value of $x$ it must be that $\phi[x_0 / x]$ holds.
If we know $\exists x \phi$ then for some value of $x$ it must be that $\phi$ holds. However, we do not know which value of $x$ makes $\phi$ hold. So we substitute $x_0$ as a generic value which cannot appear anywhere before in the proof (because we can't assume anything about $x_0$). Essentially, we are giving a name to something we know must exist, $x_0$.
My Question:
After seeing the quantifier equivalences below,
$$\neg\forall x \phi \dashv \vdash \exists x \neg \phi $$ $$\neg\exists x \phi \dashv \vdash \forall x \neg \phi $$
it seems as though we can avoid substituting a new parameter when doing $\exists$ elimination by converting $\exists x \phi$ to $\neg\forall x \neg\phi$ and applying $\forall$ elimination to it.
So using this conversion we could avoid going from $\exists x \phi$ to $\phi[c / x]$ where $c$ is a new parameter, by going from $\exists x \phi$ to $\neg\forall x \neg\phi$ to $\neg(\neg\phi[x_0 / x]) \equiv \phi[x_0 / x]$ for any term $x_0$.
How can this be allowed?
So $\exists$-elimination is used when you have $\exists x \, \phi$ available as an assumption to prove something. For example in the proof $\exists x \, \phi \vdash \alpha$ you can use it to get $\phi[t / x] \vdash \alpha$ for some term $t$.
Indeed, you can instead use the equivalence to get $\neg \forall x \, \neg\phi \vdash \alpha$, but here the leftmost negation prevents you from using the $\forall$-elimination.