Is this proof correct?
Prove $\vDash\exists x\phi\leftrightarrow\lnot\forall x\lnot\phi$
Proof: We want to see the that $\vDash\exists x\phi\leftrightarrow \vDash\lnot\forall x\lnot\phi$, so let I be an interpretation with domain |I|.
Notice that
$\vDash\exists x\phi\iff\vDash\phi[a/x],\exists a\in |I|\iff\not\vDash\lnot\phi[a/x],\exists a\in |I|\iff\not\vDash\forall x\lnot\phi \iff \vDash\lnot\forall x\lnot\phi.$
My main criticism with this is that I'd hate to see the use of quantifiers in the semantics. That is, rather than saying
$$\vDash\exists x\phi\iff\vDash\phi[a/x],\exists a\in |I|$$
I would define the semantics as:
$$\vDash\exists x\phi\iff \text{for some } a\in |I|: \ \vDash\phi[a/x]$$
That way, you have a much more clear separation between the $\exists$ as a logic symbol that is part of the logic statement you are looking at, and the 'for some' that is part of the mathematically defined semantics for that symbol.
Also, this way you can add a natural step between your step 3 and step 4 (in your proof I feel that step goes a little quick):
$$\vDash\exists x\phi\iff$$
$$\text{ for some } a\in |I|: \ \vDash\phi[a/x]\iff$$
$$\text{ for some } a\in |I|: \ \not\vDash\lnot\phi[a/x]\iff$$
$$\color{red}{\text{not for all } a\in |I|\vDash\lnot\phi[a/x]\iff}$$
$$\not\vDash\forall x\lnot\phi \iff$$
$$\vDash\lnot\forall x\lnot\phi.$$