Show that $\exists x \exists y (\varphi \land \varphi^{\frac{y}{x}} \land x \neq y)\models \forall x \exists y (\varphi^{\frac{y}{x}} \land x \neq y)$ I'm working through a book on logic and need help with the following exercise:
Show that
$\exists x \exists y (\varphi \land \varphi^y_x \land x \neq y)\models \forall x \exists y (\varphi^y_x \land x \neq y)$ where $y \notin var \; \varphi $
I know I need to show that every model for the first formula is also a model for the second but basically I don't know how to continue right after the start:
Let $M$  be a model for $\exists x \exists y (\varphi \land \varphi^y_x \land x \neq y)$. This means there are $c, d$ in the domain of $M$ such that $M^{cd}_{xy} \models  \varphi \land \varphi^y_x \land x \neq y $
And here I'm already stuck. Can someone give me a hint on how to continue?
 A: A key hint is in the entailment formula there's no conjunct $\varphi$ and $y \notin var~\varphi$. Upon your own derivation $M^{cd}_{xy} \models  \varphi(c) \land \varphi(d) \land c \neq d$ we can infer that there're at least 2 different entities in the domain of $M$ and also $\varphi$ holds at least for above two different entities from the domain, then we can show $\forall x \exists y (\varphi^y_x \land x \neq y)$ based on above background assumption and notice that $x$ is no longer a free variable of the formula $\varphi^y_x$ and for any $x$ in the domain there's always a different entity $y$ satisfying $x \neq y$ while also satisfying $\varphi$ per above argument. Of course for rigorous proof you need to invoke all allowed rules of logical consequence in your book.
A: You've started off well. If $M\models \exists xy(\varphi\land\varphi^y_x\land x\neq y)$, this means there are elements $c,d\in M$ such that $c$ satisfies $\varphi$, $d$ satisfies $\varphi$, and $c\neq d$.
Now how do we show that $M\models \forall x\exists y(\varphi^y_x\land x\neq y)$? Well, we have to show that for any $a\in M$, we can find some $b\in M$ such that $b$ satisfies $\varphi$ and $a\neq b$.
The point is that we have two distinct elements satisfying $\varphi$, so we have "room" to do this. For example, if $a\neq c$, let $b = c$. If $a = c$, let $b = d$. In either case, $b$ satisfies $\varphi$ and $a\neq b$.
