Some preliminary comments.
First: the formal expressions of the rules and their provisos may slightly differ according to the proof system: Natural Deduction, Hilbert-style, etc. Thus, it is a good practice to refer to a consistent set of rules.
Second: every proof system must be sound, i.e. it must allow us to derive only true conclusion from true premises.
Thus, for example, every proof system must avoid the following fallacy:
"Plato is a Philosopher; therefore everything is a Philosopher".
The usual proviso regarding Universal Generalization is exactly designed to avoid it.
This proviso is present also in the Natural Deduction version of the rule.
But we have to consider that the "standard" version of Natural Deduction does not have a rule like "Existential Specification": "from $\exists x Px$, derive $Pc$, for a new constant $c$".
Why so ?
Exactly in order to avoid the fallacy you have rediscovered:
"There is an Even number." Let $3$ a new name for it. Thus, from the premise above, using ES: "$3$ is Even". Now "generalize" it with UG to conclude with: "Every number is Even".
As you can see the Natural Deduction for Existential Elimination is more complicated.
Also Hilbert-style proof system, where we have the Generalization rule, cannot have Existential Specification.
Assume it; then we have (by Deduction th): $∃xPx → Pc$, and also: $∃x¬Px → ¬ Pc$.
By contraposition: $¬¬Pc → ¬∃x¬Px$ that (in classical logic) amounts to the invalid: $Pc → ∀xPx$.
You can see e.g. P.Suppes, Introduction to Logic (1957) for a detailed discussion of quantifiers rules and related restrictions.
See page 90 for the fallacy we are discussing, and see page 91 for additional restriction on UG necessary to avoid that fallacy when the system has ES.
Best Answer
You are doing this exactly right! You just have to derive $\forall y \neg P(x,y)$ from $\neg \exists y P(x,y)$
Now, I am not sure how your proof system defines the rule for $\forall$ Introduction ... in the system that I use you designate a 'fresh' constant to take the role of the arbitrary object from the domain. So this is what it looks like in my preferred system, called Fitch: