When are we allowed to use the $\exists$ elimination rule in first-order natural deduction? I don't really understand when we're allowed to use $\exists$-elimination when making first-order natural deduction proofs. I understand that the criteria are that  the variable must be free in the conclusion, and in the "context" of the implication. When reading this, I feel like I understand, but when looking at examples, I get confused. For example,
$\exists x P(x)$ and $P(x) \implies \forall y P(y)$, we cannot use the elimination rule; why is this?
Another example would be $\exists x P(x)$ and $P(x) \implies P(x)$. Here I understand that, since x is free in $P(x)$, we cannot use the elimination. However, would it be possible if we instead had $\exists x P(x)$ and $P(x) \implies \forall xP(x)$?
If so, why? Wouldn't x still be free in the context?
Any help is appreciated. Thanks!
Adding picture:

$\begin{array}{lllll}
1&1&\text{Assume }\exists x\,P(x)\land(P(x)\to\forall y\,Q(y))&\qquad\\
1&2&\exists x~P(x) &&\land E_1,1\\
1 &3& P(x)\to\forall y~Q(y)&&\land E_2,1\\
\color{red}1&4&\forall y~Q(y)&&\exists E~2, 3~\color{red}{\text{ERROR}}
\end{array}$

 A: The $\exists$-elimination rule :
$$
\frac{\begin{array}{ccc}
&&\phi[x_0/x]\\
&&\vdots\\
\exists x\phi&&\psi
\end{array}}{\psi}\exists\text{-elim}
$$
holds with the following proviso :

$x_0$ does not occur in $\psi$, $\phi$ or any undischarged assumption of the subderivation of $\psi$, except $\phi[x_0/x]$.


Here is an example showing the need for the proviso in the $\exists$-elim rule :
1) $\exists x(x=0)$ --- assumed
2) $(x=0)$ --- assumed for $\exists$-elim
3) $x=0$ --- from 2) and 1) by $\exists$-elim, discharging 2) : illegal ! $x=0$ is "the $\psi$" and we have the variable $x$ used in the $\exists$-elim application free in it
4) $\forall x(x=0)$ --- $\forall$-intro : correct ; there are no free occurrence of $x$ in the only assumption left, i.e. into 1)
5) $\exists x(x=0) \to \forall x(x=0)$ --- $\to$-intro.
The conclusion is clearly false in $\mathbb N$.

The intuition about the rule is this : we know that there is something that is $P$. Call it $x_0$ (a new term; this is required by the proviso asking for a term that does not occur in any undischarged assumption ).
Form $P(x_0)$ we derive a conclusion $\psi$ that does not "depend" on $x_0$ (and this is for sure satisfied if $x_0$ does not occur in $\psi$).
Thus, we can discard the temporary assumption $P(x_0)$ and the conclusion follows from the premise $\exists x P(x)$.


In your example, $\forall y Q(y)$ is the conclusion $\psi$ and $x$ is free into the hypothesis 1) that is an undischarged assumption of the subderivation of $\psi$.
Thus, the proviso has been violated.
A: Using my DC Proof 2.0

DC Proof will not allow the use of $x$ as both a bound and a free variable within a statement, saving much confusion. As you can see, you won't be able to apply Detachment (Modus Ponens) here.
Suggestion: Try to use the lowercase letters a-j for bound variables, the remaining lowercase letters for free variables. This also avoids some confusion.
