$ \forall x \exists y\ (P(x) \wedge Q(y)) \overset{\ ?}{\iff} \exists y \forall x\ (P(x) \wedge Q(y)) $ Is it possible to prove
$$
\forall x \exists y\ (P(x) \wedge Q(y)) \iff \exists y \forall x\ (P(x) \wedge Q(y))
$$
in a formal way. I know quantifiers do not commute in general, but do they do in this case ? I think that quantifiers always commute if the subformula is either a conjunction or disjunction of two formulas, each of them has only one of the quantfied variables.
My attempt is based on understanding the quantifiers as follows
$$
\forall x\ P(x) \iff \bigwedge_x P(x) \iff P(x_1) \wedge P(x_2) \wedge \dots \\
\exists y\ Q(y) \iff \bigvee_y Q(y) \iff Q(y_1) \vee Q(y_2) \vee \dots \\
$$
and using the distribution laws. So I proceed as follows ( I'm sorry that it is difficult to see the distribution laws in action in the presense of the big conjunction and disjunction signs)
$$
\forall x \exists y\ ( P(x) \wedge Q(y) ) \\
\bigwedge_x \left(\bigvee_y \left(Q(y) \wedge P(x)\right)\right) \\
\bigwedge_x \left(\left(\bigvee_y Q(y) \right) \wedge P(x) \right) \\
\left(\bigwedge_x  P(x) \right) \wedge \left(\bigvee_y Q(y) \right) \\
\bigvee_y \left(\left(\bigwedge_x  P(x) \right) \wedge Q(y) \right) \\
\bigvee_y \left(\bigwedge_x  \left(P(x)  \wedge Q(y) \right) \right) \\
\exists y \forall x \ ( P(x) \wedge Q(y) )
$$
 A: $\forall x\exists y~(P(x)\land Q(y))$ will be satisfied exactly when $P$ is satisfied by everything and $Q$ is satisfied by something.
Since the predicates are monovariate, we see that when some instance for $y$ satisfies $Q(y)$ then it will do so independently of the instances for $x$.  Likewise if every instance for $x$ satisfies $P(x)$, then they will do so independently of any particular instance for $y$.
Thus any interpretation will satisfy $\exists y\forall x~(P(x)\land Q(y))$ if and only if it satisfies $\exists y\forall x~(P(x)\land Q(y))$. Therefore the statements are equivalent.

Of course, this is not the case for $\forall x\exists y~R(x,y)$ and $\exists y\forall x~R(x,y)$.  There are many interpretations for $R(x,y)$ where whether it is satisfied by an instance of $y$ is not independent of the instance for $x$.  For example: when $R(x,y)$ is interpreted as $(x<y)$.
So not all interpretations which satisfy $\forall x\exists y~R(x,y)$ will also satisfy $\exists y\forall x~R(x,y)$.
