Is it necessary to remove implications/bi-implications before converting to prenex normal form? I read: I don't think the first step is necessary. Can anyone prove or disprove providing a counterexample that we reach non-equivalent predicate formulas?

Kind of formulas I'm talking about are:
$$\exists u((\exists x(A(x)\implies\forall y B(x,y)))\implies(\exists zC(z)\implies\forall B(u,w)))$$
or:
$$((\exists x_1A(x_1)\wedge\exists x_2B(x_2))\implies\exists x_3C(x_3))\implies \exists x_4D(x_4)$$
 A: Step 1 should be written explicitly as convert all sub expressions of the form $A \iff B$ into $A \implies B \land B \implies A$, and then convert all sub expressions of the form $A \implies B$ into $\lnot A \lor B$.
If you skip step (1), then step (4) won't work.  This is because, for example:
$$\begin{array} {rl}
%
(\forall x~A(x)) \implies B &= \lnot(\forall x~A(x)) \lor B \\
%
&= (\exists x~ \lnot A(x)) \lor B \\
%
&= \exists x~ (\lnot A(x) \lor B) \\
%
&= \exists x~ (A(x) \implies B) \\
%
\end{array}$$
The point is that it is not always the case that $(\forall x~A(x)) \implies B$ is logically equivalent to $\forall x~(A(x) \implies B)$.  So a counter example would be any instance of 
$$(\forall x~A(x)) \implies B$$
where $\exists x~ (A(x) \implies B)$ isn't equivalent to $\forall x~ (A(x) \implies B)$.  So for counter example, $A(x)$ is $x=1$ and $B$ is $1=1$.
So you can't just move quantifiers to the front of a formula unless all $\lnot$s are all on the leaves, and the only other boolean operators present are $\lor$ and $\land$.
Aside, hopefully your text mentions somewhere that this algorithm only works in a nonempty universe, since
$$A \land \forall x ~ B(x) = \forall x ~ A \land B(x)$$
doesn't hold when $A$ is false and the universe is empty.  This post should help explain the reasoning behind the above algorithm.
A: You don't have to eliminate implications or move negations in, but the rule for moving the quantifiers out needs to take them into account: to do this you use the following equivalences
$$
\begin{array}{rcl}
(\exists x(A(x)) \to B &\equiv& \forall x(A(x) \to B)\\
(\forall x(A(x)) \to B &\equiv& \exists x(A(x) \to B)\\
A \to (\exists x(B(x)) &\equiv& \exists x (A \to B(x))\\
A \to (\forall x(B(x)) &\equiv& \forall x (A \to B(x))\\
\lnot(\exists x(A(x))) &\equiv& \forall x (\lnot(A(x)))\\
\lnot(\forall x(A(x))) &\equiv& \exists x (\lnot(A(x)))\\
\end{array}
$$
(with bound variables renamed as necessary to avoid variable capture). What is happening here is that existential quantifiers in negative positions (left-hand operand of $\to$, operand of $\lnot$) become universal when you move them out and vice versa when you move universal quantifiers out. In positive positions (right-hand operand of $\to$, either operand of $\lor$ or $\land$) the quantifiers stay the same when you pull them out.
You have to expand $A \leftrightarrow B$ into $(A \to B) \land (B \to A)$, because $A$ and $B$ appear both positively and negatively in $A \leftrightarrow B$.
