I am trying to convert $∃x∀y(p(x, y) ⟺ q(x))$ into prenex conjunctive normal form.
These are the steps that I have taken thus far, however feel that I am missing something or went wrong somewhere.
Eliminate →, ⟺ and import negations
= ∃x∀y(p(x, y) → q(x)) ⋀ (q(x) → p(x, y))
= ∃x∀y(¬p(x, y) ⋁ q(x)) ⋀ (¬q(x) ⋁ p(x, y))
= ∃x∀y(p(x, y) ⋁ q(x)) ⋀ (¬q(x) ⋁ p(x, y)) * Renaming and using equivalences (b) – (c)
= ∀x∀y(p(x, y) ⋁ q(x)) ⋀ (¬q(x) ⋁ p(x, y)) * Resulting prenex CNF