Does $\exists x\forall yQ(x,y) \to \forall y\exists xQ(x,y)$? Consider the following examples,

*

*$x$ loves $y$, where $x$ and $y$ are humans

somebody loves everybody $\to$ everybody is loved by somebody


*$x$ can open $y$, where $x$ are keys and $y$ are locks

some keys can open all locks $\to$ all locks can be opened by some keys
But does "$\exists x\forall yQ(x,y) \to \forall y\exists xQ(x,y)$" always hold true?
 A: Yes.
One way to prove this is by using a proof tree. You start with the negation of the formula in question then apply a series of contradiction hunting rules to show that, no matter what, that negation is false, like so:

This tree was generated here.
A: Intuitively, the answer has to be yes: The leading term asserts that there is a common $x$ satisfying $Q(x,y)$ for every $y$, while the trailing term asserts that for every $y$ there is some $x$ satisfying $Q(x,y)$. For the trailing term, there is no reason why it cannot be the same $x$ for each $y$.
A: Formal Proof
We have the axiom
$$
\forall x (\varphi \to \psi(x)) \to (\varphi \to \forall x \psi(x)) \tag{$Q1$}
$$
from which we can deduce
$$
\forall x (\psi'(x) \to \varphi') \to (\exists x \psi'(x) \to \varphi') \tag{$Q1'$}
$$
via $Q3$: $\exists x \varphi(x) \leftrightarrow \neg\forall x \neg \varphi(x)$ and the tautology $(p \to q) \leftrightarrow (\neg q \to \neg p)$.
From $Q2$: $ \varphi(x) \to \exists x \varphi(x)$ we get $Q2'$: $ \forall x \varphi(x) \to \varphi(x)$.
\begin{align*}
 \varphi_0 & :Rxy \to \exists x Rxy &  & Q2\\
 \varphi_1 & :\forall y Rxy \to Rxy &  & Q2'\\
 \varphi_2 & :(Rxy \to \exists x Rxy)\land(\forall y Rxy \to Rxy)   & &  \varphi_0 \land \varphi_1\\
 \varphi_3 & :(Rxy \to \exists x Rxy)\land(\forall y Rxy \to Rxy) \to (\forall y Rxy \to \exists x Rxy) &  & ((p \to q)\land (q \to r)) \to (p \to r)\\
 \varphi_4 & :\forall y Rxy \to \exists x Rxy &  & \text{MP}(\varphi_2,\varphi_3) \\
 \varphi_5 & :\forall x(\forall y Rxy \to \exists x Rxy) &  & \text{Generalisation}(\varphi_4) \\
 \varphi_6 & :\forall x(\forall y Rxy \to \exists x Rxy) \to (\exists x\forall y Rxy \to \exists x Rxy) &  & Q1' \\
 \varphi_7 & :\exists x\forall y Rxy \to \exists x Rxy &  & \text{MP}(\varphi_5,\varphi_6) \\
 \varphi_8 & :\forall y(\exists x\forall y Rxy \to \exists x Rxy) &  & \text{Generalisation}(\varphi_7) \\ 
 \varphi_9 & :\forall y(\exists x\forall y Rxy \to \exists x Rxy) \to (\exists x\forall y Rxy \to \forall y\exists x Rxy) &  & Q1 \\
 \varphi_{10} & :\exists x\forall y Rxy \to \forall y\exists x Rxy &  & \text{MP}(\varphi_8,\varphi_9) \\
\end{align*}
