Assuming you need (Ǝx ~P(x)) ---> ~∀x P(x), an informal proof is as follows. Assume Ǝx ~P(x) and break into into some x and a proof of ~P(x) using existential elimination. To prove ~∀x P(x), assume ∀x P(x). Instantiate it with x to get P(x). It gives a contradiction with ~P(x). Closing the assumption ∀x P(x), we get ~∀x P(x).
Do you need a Fitch-style or tree-like derivation?