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$