Is there a proof of $\lnot \forall x, P(x) \iff \exists x, \lnot P(x)$ I am interested in how one would formally prove:
$\lnot \forall x, P(x) \iff \exists x, \lnot P(x)$
I realize that it's basically saying that:
$\lnot(P(x_0) \land P(x_1) \land ... \land P(x_n)) \iff \lnot P(x_0) \lor \lnot P(x_1) \lor ... \lor \lnot P(x_n)$
Which is an "intuitive" proof assuming we already accept De Morgan's, but I am curious if there is a formal way to prove it (e.g. Fitch-style). 

Fitch style proof:
\begin{array}{lll}
1&\neg \forall x \ P(x) & Assumption\\
2&\quad \neg \exists x \ \neg P(x)&Assumption\\
3&\quad \quad a&\\
4&\quad \quad \quad \neg P(a) & Assumption\\
5&\quad \quad \quad \exists x \ \neg P(x)&\exists \ Intro \ 4\\
6&\quad \quad \quad \bot& \bot \ Intro \ 2,5\\
7&\quad \quad \neg \neg P(a)& \neg \ Intro \ 4-6\\
8& \quad \quad P(a)& \neg \ Elim \ 7\\
9&\quad \forall x \ P(x) & \forall \ Intro \ 3-8\\
10&\quad \bot & \bot \ Intro \ 1,9\\
11&\neg \neg \exists x \ \neg P(x)&\neg \ Intro \ 2-10\\
12&\exists x \ \neg P(x)&\neg \ Elim \ 11\\
\end{array}
Conceptual explanation: the basic strategy is to prove this by a proof by contradiction. That is, if it is not the case that there is some non-P, then everything is a P, which contradicts the assumption that not everything is a P.
