Prove that $\exists z \in \mathbb{R} \forall x \in \mathbb{R}^+ [\exists y \in \mathbb{R} (y-x = y/x) \iff x \neq z]$ 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$
 A: 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".
A: To prove an existence, you must either directly construct an example, or indirectly prove that non-existence reduces to absurdity.   NB: for this exercise you should do the former.
You may not just "Let $z=0$," because you have no assurance that zero may be a witness to the existential.
Your task is to find some real value, $z$, for which any arbitrary positive real value, $x$, will have a real valued solution for $y$ in $(y-x=y/x)$ exactly when $x\neq z$ . 

 Well we know that for any positive $x$, the $y$ solution to $y-x=y/x$ is $x^2/(x-1)$.  So ...

