I was wondering how the distribution of the negation works on a nested quantifier, taking into consideration the equivalent formulations.
This is what I mean. I have this sentence:
$\forall x(Ax\rightarrow\exists y(Bxy\wedge\neg Ay)).$
This is, following the equivalent sentence forms rule $(\forall x(P\rightarrow Q)\equiv\neg\exists x(P\wedge\neg Q))$, equal to
$\neg\exists x(Ax\wedge\neg\exists y(Bxy\wedge\neg Ay))$
$\neg\exists x(Ax\wedge\forall y(Bxy\rightarrow Ay)).$
Is it legitimate to pose the subformula $\exists(Bxy\wedge\neg Ay)$ as “Q” in the meta-formula $\forall x(P\rightarrow Q)$? Is, thus, the reasoning correct?