Transform the given formula $(\exists{x})a(x) \Leftrightarrow (\forall{x})\ b(x,y) $ ... Transform the formula, so that all the quantifiers are at the beginning
$$(\exists{x})a(x) \Leftrightarrow (\forall{x})\ b(x,y) $$
I tried to do it this way:
$$ ((\exists{x})a(x) \Leftrightarrow \forall{x}\ b(x,y))\Leftrightarrow \lnot (\forall{x} \lnot a(x)) \Leftrightarrow  (\forall{z})\ b(z,y) \Leftrightarrow (\lnot (\forall{x}))(\forall{z})(a(x)\Leftrightarrow b(z,y)).$$
But I am pretty sure it's wrong and the negation can't be extracted this way. Can anyone help me with this?
 A: You have $$((\exists{x})a(x) \Leftrightarrow \forall{x}\ b(x,y))\Leftrightarrow \lnot (\forall{x} \lnot a(x)) \Leftrightarrow  (\forall{z})\ b(z,y) \Leftrightarrow (\lnot (\forall{x}))(\forall{z})(a(x)\Leftrightarrow b(z,y))$$
There is no reason to "doubly negate" the existential quantifier when moving from your first to second implication. Furthermore, care must be taken when extracting quantifiers from a quantified antecedent of an implication, and moving those quantifiers to the front of the entire implication.
Precision is everything, in logic (and in math)!
It would be much more straightforward to simply proceed as follows, starting with the statement you want to transform:

Assuming $y$ is not quantified, i.e., treating $y$ is a constant, we have:
$$(\exists{x})a(x) \Leftrightarrow (\forall{x})\ b(x,y)\tag{1}$$
Then $(1)$ is equivalent to the conjunction of two implications, each of which needs distinct variables, we'll use $x$ and $z$ for the forward direction, and $s, t$ for the reverse direction:
$$[(\exists{x})a(x) \rightarrow (\forall{z})\ b(z,y)] \land [(\forall{s})\ b(s,y) \rightarrow (\exists{t})a(t)]\tag{2}$$
Given that we want to pull out the existential quantifier from the antecedent of first implication, we need to change it to a univeral quantifier of the variable $x$; likewise we need to reverse the existential quantifier in the antecedent of the second implication. With this in mind, $(2)$ is equivalent to 
$$(\forall{x})(\forall{z})[a(x) \rightarrow \ b(z,y)] \land (\exists{s})(\exists{t})[b(s,y) \rightarrow a(t)]\tag{3}$$
Now we can pull the quantifiers to the front; that is, $(3)$ is equivalent to
$$(\forall{x})(\forall{z})(\exists{s})(\exists{t})\{[a(x) \rightarrow \ b(z,y)] \land [b(u,y) \rightarrow a(v)]\}\tag{4}$$

A: Let's assume you indeed meant the unquantified $y$. Then
$$(\exists{x})a(x) \leftrightarrow (\forall{x})\ b(x,y)$$
is equivalent to
$$[(\exists{x})a(x) \rightarrow (\forall{z})\ b(z,y)] \land [(\forall{u})\ b(u,y) \rightarrow (\exists{v})a(v)]$$
is equivalent to
$$(\forall{x})(\forall{z})[a(x) \rightarrow \ b(z,y)] \land (\exists{u})(\exists{v})[b(u,y) \rightarrow a(v)]$$
is equivalent to
$$(\forall{x})(\forall{z})(\exists{u})(\exists{v})\{[a(x) \rightarrow \ b(z,y)] \land [b(u,y) \rightarrow a(v)]\}$$
though indeed, in this special sort of case, the now initial quantifiers can be reordered. 
