Proof regarding logic and negation of quantifiers I've read about the following task, but don't know how to prove it:
Proof that $\neg(\forall  x ( V(x)\rightarrow F(x))\iff \exists x( V(x) \land \lnot F(x)) $.
Maybe we start by proving "$\Leftrightarrow$" by proving the contraposition:
$\neg\exists x (V(x) \land \lnot F(x)) \Rightarrow \forall  x ( V(x)\rightarrow F(x))$
Now we can make a contradiction by assuming:
$\exists x (V(x)\land \lnot F(x))$  but how do I move on now?
 A: I don't know how you are supposed to prove this (Formal proof? Using equivalences? Some other method?), but let me do one that uses the following basic equivalences:
$\neg \forall x \varphi(x) \Leftrightarrow \exists x \neg \varphi(x)$ (Quantifier Negation)
$\varphi \rightarrow \psi \Leftrightarrow \neg \varphi \lor \psi$ (Implication)
$\neg(\varphi \lor \psi) \Leftrightarrow \neg \varphi \land \neg \psi$ (DeMorgan)
$\neg \neg \varphi \Leftrightarrow \varphi $ (Double Negation)
OK, using these, we get:
$\neg \forall x (V(x) \rightarrow F(x)) \Leftrightarrow $ (Quantifier Negation)
$\exists x \neg (V(x) \rightarrow F(x)) \Leftrightarrow $ (Implication)
$\exists x \neg (\neg V(x) \lor F(x)) \Leftrightarrow $ (DeMorgan)
$\exists x (\neg \neg V(x) \land \neg F(x)) \Leftrightarrow $ (Double Negation)
$\exists x (V(x) \land \neg F(x)) $ 
A: $\neg(\forall  x ( V(x)\rightarrow F(x))$ is equivalent with the following statement:
P: there exists at least one $x^*$, such that $V(x^*)$ does not imply $F(x^*).$
"$V(x^*)$ does not imply $F(x^*)$" is equivalent with "$V(x^*)$ and $F(x^*)$ both being true."
Thus P can be written as $\exists x( V(x) \land \lnot F(x)).$
A: Here is an approach to proving the biconditional using a Fitch-style proof checker. Using a proof checker makes sure that I am following the rules.

I used the following rules: change of quantifiers (CQ), universal elimination (∀E), universal introduction (∀I), De Morgan's laws (DeM), negation elimination (¬E), negation introduction (¬I), disjunctive syllogism (DS), double negative elimination (DNE), conditional introduction (→I), conditional elimination (¬E), indirect proof (IP), existential elimination (∃E) and biconditional introduction (↔I).

Kevin Klement's JavaScript/PHP Fitch-style natural deduction proof editor and checker http://proofs.openlogicproject.org/
