I have problems with the following proof: $$ \forall x \exists y (Rxy \land Py), \forall x \neg Rxx \vdash \neg \forall x \forall y (Px \implies (Py \implies x=y)) $$ The problem is with the application of the existential elimination rule - no matter what, there are other undischarged assumptions which prevent me from applying the rule.
Edit: The empty structure is not a valid domain
Not sure what system you are using, but here is a proof in Fitch: