How to prove this formula? $$\forall x[p\vee\Phi(x)]\;\Longleftrightarrow\; [p\vee\forall x[\Phi(x)]$$ where $p$ does not contain $x$ as a free variable.
I was reading Set theory by K. Kuratowski, A. Mostowski when I encountered this formula. The book says that it's easy to check. Well, I can prove the left arrow:
\begin{align} [p\vee\forall x[\Phi(x)] &\Longleftrightarrow[\forall xp\vee \forall x[\Phi(x)] && (\forall xp\Longleftrightarrow p)\\ [\forall xp\vee\forall [\Phi(x)] & \implies \forall x[p\vee\Phi(x)] &&([\forall x\Phi(x)\vee\forall x\Psi(x)]\Rightarrow \forall x[\Phi(x)\vee\Psi(x)]) \end{align}
But I haven't got any idea how to prove the right arrow. I know an informal 'proof' using the fact that if a,b,c,... denote the objects in my domain then
$∀xP(x)≈P(a)∧P(b)∧P(c)∧...$
$∃xP(x)≈P(a)∨P(b)∨P(c)∨...$
But I think that's not what the book suppose. How to prove the right arrow?
Your above effort is almost done to prove the equivalence for both directions, you only need to additionally realize $\forall xp\vee\forall \Phi(x) \implies \forall x[p\vee\Phi(x)]$ actually can be strengthened to $\forall xp\vee\forall \Phi(x) \Longleftrightarrow \forall x[p\vee\Phi(x)]$ when $p$ has no free occurrence of $x$. Also note in FOL the above equivalence with disjunction form doesn't hold in general, but its conjunction form always holds.
When formula $p$ has no free occurrence of $x$, $\forall x[p\vee\Phi(x)]$ is true if $p$ is true (which doesn't depend on $x$), or if $\forall x \Phi(x)$ is true, or both are true. So it's easy to check that this imposes the same truth conditions on both $p\vee\forall \Phi(x)$ and $\forall xp\vee\forall \Phi(x)$. Formally you can use $\forall$-elim, $\lor$-elim, and $\forall$-intro rules to syntactically derive if you can use a natural deduction system or similar rules in a Hilbert system.