I have been struggling with knowing when it is okay to reuse variables within a proof. For example, in my proof below is it valid to existentially instantiate $y$ after I state $\exists y \in \mathbb{R} (y-x = y/x)$?
Proof: Let $z = 0$. Let $x \in \mathbb{R}^+$ be arbitrary. Suppose $\exists y \in \mathbb{R} (y-x = y/x)$. Thus, we can choose a $y \in \mathbb{R}$ such that $y-x = y/x$. Suppose $x = z$. Since $z=0$, $x=0$. Then we have $y-0=y/0$, but $y/0$ is undefined, so we have a contradiction. Thus, $x \neq z$. Therefore, if $\exists y \in \mathbb{R} (y-x = y/x)$, then $x \neq z$.
Now suppose $x \neq z$. Let $y = \frac{x}{1-1/x}$. $y$ is defined since $x \neq z = 0. $ Then we have $y-x=\frac{x}{1-1/x}-x = \frac{x}{1-1/x} - \frac{x-1}{1-1/x} = \frac{1}{1-1/x} = \frac{x}{1-1/x} * \frac{1}{x} = \frac{y}{x}$. Thus, $\exists y \in \mathbb{R} (y-x = y/x)$. Therefore, if $x\neq z$, then $\exists y \in \mathbb{R} (y-x = y/x)$.
Since $x$ was arbitrary, it follows that $\forall x \in \mathbb{R}^+ [\exists y \in \mathbb{R} (y-x = y/x) \iff x \neq z]$. Thus, there $\exists z \in \mathbb{R} \forall x \in \mathbb{R}^+ [\exists y \in \mathbb{R} (y-x = y/x) \iff x \neq z]$. $\square$
Okay, $x$ can be any positive real.
So let's solve for $y$ when $y - x = \frac yx$ so $y-\frac yx = x$ so $y(1-\frac 1x) = x$.
Assuming $1-\frac 1x \ne 0$. then $y =\frac x{1-\frac 1x}$ will be a solution.
But if $1-\frac 1x = 0$ or in other words if $x = 1$ then $y-x = \frac yx$ would mean $y-1 = y$ which has no solutions.
So for every $x\in \mathbb R^+$ then $y-\frac yx = x$ will have a solution if and only if $x\ne 1$.
So $z = 1$ is such a number that does what you want.
.....
The problem with $z = 0$ is that,1) $x =z=0\not \in \mathbb R^+$ and 2) yes, if $x=0$ then $y-x =\frac yx$ has not solution, but $x\ne 0$ does not guarantee a solution. You have the "if" but not the "only if".