Question About Null Quantification Equivalences

This is a well known result regarding implication during prenex normal form conversion:

these rules require that the variable quantified in one subformula does not appear free in the other subformula.

The rules for removing quantifiers from the antecedent are (note the change of quantifiers):

$(\forall x\phi) \rightarrow \psi$ is equivalent to $\exists x(\phi \rightarrow \psi )$...

So your 2nd direction can be easily shown correct too per above rule. Finally how to rigorously prove such rule? The same reference talks about the idea right above it:

These rules can be derived by rewriting the implication $\phi \rightarrow \psi$ as $\lnot \phi \lor \psi$ and applying the rules for disjunction above.