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) ) $$
$\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)$.