Handbook of Automated Reasoning

Proof

Let $\mathcal{M}=\langle \mathcal{D},\mathcal{I},\nu \rangle$ be an interpretation and define

${\mathcal{S}}^{\varphi }({\overline{b}}_n)=\{{\overline{a}}_k|\mathcal{M}[{\overline{y}}_n/{\overline{b}}_n,{\overline{x}}_k/{\overline{a}}_k]\models \varphi \}$

Since $\mathcal{M}\models \exists {\overline{x}}_k(\varphi \wedge \psi )$ ,we know that ${\mathcal{S}}^{\varphi }(\nu ({\overline{y}}_n))\ne \varnothing$ , where $\nu ({\overline{y}}_n)$ abbreviates the sequence ν(y ₁),…,ν(y _n). Thus we ...