∀y (Py ⇔ a=y) ⊨ ∃y (Pb ∧ Py ∧ ¬b=y)

[ ∃y(Pb ∧ Py ∧ ¬b=y) ]
---------------
Pb ∧ Pc ∧ ¬b=c
---------------
Pc ∧ ¬b=c
----------------
¬b=c
-------------------
¬∃y(Pb ∧ Py ∧ ¬b=y)