On the Wikipedia page for First-order logic, there is a list of Provable Identities. Although they seem very basic, I can't find anyone giving a formal proof of them.
In particular, consider one direction of one of these identities:
$$\lnot \forall a. P(a) \to \exists b. \lnot P(b)$$
What are some strategies to prove this statement -- that is, how do I 'work' with the negation of a quantifier?