Is this the correct way to prove $\exists y \forall x (P(x) \vee Q(y)) \equiv \forall xP(x) \vee \exists x Q(x)$? $\exists y \forall x (P(x) \vee Q(y)) \equiv \forall xP(x) \vee \exists x Q(x)$
If the LHS is true, then there are two cases: P(x) is true, in which case $\forall$ P(x) is true and the RHS is true, and Q(y) is true, in which case $\exists$ x Q(x) is true and the RHS is true.
If the RHS is true, then there are two cases $\forall$ P(x) is true, in which case P(x) is true and the LHS is true, and $\exists$ x Q(x) is true, in which case Q(y) is true and the LHS is true.
 A: I think the easiest way to prove this is to use the rules for manipulating quantifiers. Starting with the LHS, we have
$$
\begin{align*}
\exists y[\forall x(P(x)\vee Q(y))] &\equiv \exists y [\forall x P(x) \vee \forall x Q(y)]\\
&\equiv \exists y [\forall x P(x) \vee Q(y)] \\
&\equiv \exists y\forall x P(x) \vee \exists y Q(y) \\
&\equiv \forall xP(x) \vee \exists yQ(y) \\
&\equiv \forall xP(x) \vee \exists xQ(x).
\end{align*}
$$
This is because $\mathbf{Q}\mathbf{v}(\mathbf{P}(\mathbf{v})\ \mathbf{B}\ \phi)\equiv (\mathbf{Q}\mathbf{v}\mathbf{P}(\mathbf{v}))\ \mathbf{B}\ \phi$ is valid where $\mathbf{Q}$ is a quantifier, $\mathbf{v}$ is a variable, $\mathbf{P}$ is a predicate, $\mathbf{B}$ is either the conjunction or disjunction operator, and $\phi$ is a formula where $\mathbf{v}$ isn't free.
For your proof, when assuming the LHS, splitting directly into cases isn't possible because the disjunction is "trapped" by the quantifiers. We must say: let $c$ be an object such that $\forall x(P(x)\vee Q(c))$ is true (we know such a $c$ exists because of the assumption). Now let $a$ be an arbitrary object. We know $P(a)\vee Q(c)$ is true. Suppose now that $Q(c)$ is true. Then certainly $\exists xQ(x)$. Now suppose $P(a)$ is true. Since $a$ was arbitrary, $\forall xP(x)$ is true.
