The Order of Mixed Quantifiers How can we derive the implication:
$$ ∃y∀xP(x,y) \implies ∀x∃yP(x,y) $$
In other words, when quantifiers in the same sentence are of the same type (all
universal or all existential), the order in which they occur does not
matter. But when they are mixed, the order in which they occur becomes
crucial.
How does the above formula hold?
 A: We can formally prove that:
$$ \exists y \forall x P(x,y) \implies \forall x \exists y P(x,y) $$
but the reverse implication is not logically valid.
Consider the $y$ promised by the first statement, a $y$ which satisfies $P(x,y)$ for every $x$.  From this it may be seen that for every $x$, some $y$ exists such that $P(x,y)$.  That is the informal restatement of the above.
But the reverse implication is not provable as can be seen from the following example.  Suppose that $P(x,y)$ is interpreted in the domain of natural numbers as "x is less than y".  Then for every $x$, certainly there exists $y$ such that $x$ is less than $y$.  Thus it is the case that $\forall x \exists y P(x,y)$.  However with this interpretation, the first statement $\exists y \forall x P(x,y)$ would mean that some $y$ is greater than every number $x$, a clear impossibility (e.g. a number cannot be greater than itself).
A: Both statements are not equivalent.
As a rule of thumb, in such a sentence,  the variables after the $\exists$ symbols depends on every variable declared before. Here, using this rule yields
$$
\exists y\ \ \forall x\ \ P(x,y)\\
\forall x\ \ \exists y(\color{red} x)\ \ P(x,y)
$$
From here you see that there is no equivalence, but that the first implies the second.
A: They are different statements, in general. The second statement says that for every $x$ there is some $y$ such that $P(x,y)$ holds, while the first states that the same $y$ has $P(x,y)$ hold for every $x$.
For example, say we consider the property $x \leq y$, talking about integers. Then $(\forall x)( \exists y)(x \leq y)$ is true - we can take $y = x$. But $(\exists y)(\forall x)(x \leq y)$ is false, because for any given $y$ there is some $x$, say $y+1$, with $x \not \leq y$.
A: For me, this was one of the most difficult principles in predicate logic to apply, especially in longer proofs with many variables and sub-proofs. To establish the principle involved, I think it really helps to make the domain of quantification explicit for every quantifier as they do in mathematics. Consider the following examples.

Example 1
Venturing into the realm of science fiction here, suppose there is a female that is the mother of all males:
$$\exists a\in F: \forall b\in M: Mother(a,b)$$
where $F$ is the set of all females, $M$ is the set of all males, and $Mother(a,b)$ means $a$ is the mother of $b$.
Switching the quantifiers around, it should then be obvious that, even in this strange world, every male would have a mother: 
$$\forall b\in M: \exists a\in F: Mother(a,b)$$

Example 2
More realistically, suppose to begin with that every male has a mother:
$$\forall b\in M: \exists a\in F: Mother(a,b)$$
It should be obvious then that we cannot infer from this that every male has the same mother. In this case, we cannot just switch the quantifiers around to obtain: $$\exists a\in F: \forall b\in M: Mother(a,b)$$.

You can "reason it out" in simple, less abstract cases like this, but I initially found it very difficult and cumbersome to formalize this principle to be broadly applied. 
It may not be much help in logic courses where you must follow the exact formalism given, but if you are more interested in mathematical proofs where there is some leeway, readers may be interested in my own solution that greatly simplifies such matters. It is implemented in the form of an automated proof assistant available at my website. 
