I'm trying to prove the following:
$\neg\forall xP(x) \equiv \exists x \neg P(x)$.
So I tried to prove $\neg\forall xP(x) \models \exists x \neg P(x)$ and $\exists x \neg P(x) \models \neg\forall xP(x) $.
My work so far:
For $\neg\forall xP(x) \models \exists x \neg P(x)$:
It's enough to prove $\models \neg\forall xP(x) \rightarrow\exists x \neg P(x)$
Suppose $\models \neg(\neg\forall xP(x) \rightarrow\exists x \neg P(x))$, then
1)$\neg\forall xP(x)$
2)$\neg(\exists x \neg P(x)))$
3)$\neg(\neg\forall x \neg \neg P(x))$ (substituting $\exists x$ with $\neg \forall x \neg$
4)$\neg(\neg \forall x P(x))$ (double negative substitution)
and we have a contradiction between 1) and 4), so it must be $\models \neg\forall xP(x) \rightarrow\exists x \neg P(x)$.
I'm not really sure if the proof above is valid.
In almost every presentation of first-order logic that I have seen, one of the following is provided as an axiom schema or definition of quantification...
$$\forall x.\varphi(x)\equiv\neg\exists x.\neg\varphi(x)\qquad\text{or}\qquad\exists x.\varphi(x)\equiv\neg\forall x.\neg\varphi(x)$$
If you have this axiom, then it is trivial to show that $\neg\forall x.P(x)\equiv\exists x. \neg P(x)$
$$\begin{align} \quad\forall x.\varphi(x)\equiv\neg\exists x.\neg\varphi(x)&\quad\to\quad\neg\forall x.\varphi(x)\equiv\neg\neg\exists x.\neg\varphi(x)\\ &\quad\to\quad\quad\neg\forall x.\varphi(x)\equiv\exists x.\neg\varphi(x) \end{align}$$
$$\begin{align} \quad\exists x.\varphi(x)\equiv\neg\forall x.\neg\varphi(x)&\quad\to\quad\exists x.\neg\varphi(x)\equiv\neg\forall x.\neg\neg\varphi(x)\\ &\quad\to\quad\exists x.\neg\varphi(x)\equiv\neg\forall x.\varphi(x)\\ &\quad\to\quad\neg\forall x.\varphi(x)\equiv\exists x.\neg\varphi(x) \end{align}$$
Instantiate $\varphi$ as $P$, and you have your proof.
If you do not have the stated axiom schema, then you can derive it using natural deduction (see the linked answer) or semantic tableaux (these approaches are equivalent).
Since the comments and linked question pretty much cover this, here's a less-standard approach that hopefully offers a bit more insight into the intuition underlying why the equivalence makes sense.
In the finite case, the quantifiers $\forall$ and $\exists$ can be defined according to...
$$\forall x.P(x)\equiv\bigwedge_{i\in[n]}P(x_i)\equiv P(x_0)\land P(x_1)\land P(x_2)\land\cdots\land P(x_n)$$
...and...
$$\exists x.P(x)\equiv \bigvee_{i\in[n]}P(x_i)\equiv P(x_0)\lor P(x_1)\lor P(x_2)\lor\cdots\lor P(x_n)$$
By the application of De Morgan's law, we have that...
$$\neg\bigwedge_{i\in[n]}P(x_i)\equiv\bigvee_{i\in[n]}\neg P(x_i)$$
...whence,...
$$\neg\forall x. P(x)\equiv \exists x.\neg P(x)$$
As it so happens, there are consistent, infinitary logics, which have an accompanying infinitary De Morgan's law, in which the above can be applied over an infinite domain.