The constraints of Universal Introduction in logic proofs

Using existential elimination properly is more nuanced than that.

In natural deduction, existential elimination says that from $\exists x\varphi(x)$ and $\varphi(y)\to\psi$, that you can infer $\psi$, as long as $y$ doesn't exist in $\psi$ or $\exists x\varphi(x)$ or any of your hypotheses.

I believe the reason that Wikipedia is as simplistic as it is is because there are formulas of first-order logic in which existantial elimination (or existential instantiation) as a single step is as simple as it is stated there. For instance, this was the case in Andrew's formulation in To Truth Through Proof.

However, the rule of inference I mention above is also in the system by a different name. (In Andrews, it is called Rule C.) In his system, existential instantiation and Rule C are bookends of choosing a variable and then "releasing" it at the end. In Fitch, by contrast, you choose a variable in an assumption and then release it by $\exists E$, which in practice is a lot less drama in my experience.

You have made an error in your second step. This is one reason I like a certain style that I believe had been introduced by Fitch. I learned it in "Symbolic Logic" by James Thomas. It uses vertical lines alongside of proof steps to keep track of subsidiary assumptions.

The formula in your second step is a subsidiary assumption. Discharging it will give you 'P implies P'. Applying the universal introduction before the discharge will give you

$$\varphi(y) \to (\forall x ( \varphi(x)))$$

after the discharge. But this is just an instance of universal generalization, itself. So, it is true by stipulation of the logical axioms, and, it can take any formula as an antecedent.