Convert predicate to prenex normal form $$\color{red}{(}\neg A(x)\lor \exists x\text{ }\color{green}{(}\forall y\text{ } B(x,y) \to \exists y \text{ }C(x,y)\color{green}{)}\color{red}{)}$$ So far I could only perform the following operation: $$\color{red}{(}\neg A(x)\lor \exists x\text{ }\color{blue}{(}\exists y\text{ }\color{green}{(} B(x,y) \to \text{ }C(x,y)\color{green}{)}\color{blue}{)}\color{red}{)}$$ I can't really factor out the $\exists x$ because $x$ is **free** in $\neg A(x)$. What know?

You are right that you cannot move the $\exists x$ over the $\
eg A(x)$.

But you can rename variables!

So, you could replace the $x$ in $A(x)$ with a $z$, and now bring the $\exists x$ out.

Remember, variables are just dummy placeholders.