Prove the following for a general binary operation, $\Delta$ I would like somebody to confirm if my proof is correct or not, please.
The question below:

Prove the following for a general binary operation $\Delta$:
  \begin{equation}
    \left[ \forall_{x} \exists_{y} [y \Delta y = x] \right] \implies \left[ \forall_{x} \exists_{a} \exists_{b} \left[ (a \Delta a) \Delta b = x \right]\right]
\end{equation}

My proof:
\begin{align}
    1&. \quad \forall_{x} \exists_{y} [y \Delta y = x] \tag{assume} \\
    2&. \quad x \tag{declare} \\
    3&. \quad a = c \tag{choose} \\
    4&. \quad b = c \Delta c \tag{choose} \\
    5&. \quad ( c \Delta c ) \Delta ( c \Delta c ) = x \tag{1,3,4} \\
    6&. \quad \exists_{b} \left[ (a \Delta a) \Delta b = x \right] \tag{4,5} \\
    7&. \quad \exists_{a} \exists_{b} \left[ (a \Delta a) \Delta b = x \right] \tag{3 $\to$ 6} \\
    8&. \quad \forall_{x} \exists_{a} \exists_{b} \left[ (a \Delta a) \Delta b = x \right] \tag{2 $\to$ 7} \\
    9&. \quad \left[ \forall_{x} \exists_{y} [y \Delta y = x] \right] \implies \left[ \forall_{x} \exists_{a} \exists_{b} \left[ (a \Delta a) \Delta b = x \right]\right] \tag{1 $\to$ 8}
\end{align}
An explanation of my thought process follows (line numbers correspond to that of the proof's):


*

*We assume this part.

*Because we can't continue due to the assumption's $ \forall $ we start working backwards. Thus, we start using the conclusion's $\forall_{x} \exists_{a} \exists_{b}$. With the first part being $\forall_{x}$, we declare $x$.

*From the next $\exists_{a}$, we choose a value for $a$. Because we are working with a general set of objects as values, we assign it a specific value called $c$.

*From the next $\exists_{b}$, we, similarly, choose a value for $b$. We choose it to be $(c \Delta c)$, because we will be using the fact that for all $x$ there exists a value $y$ such that $y \Delta y = x$. 

*Thus, the reason we choose $b$ to be $(c \Delta c)$, is because, when we substitute the values of $a$ and $b$ into $(a \Delta a) \Delta b = x$ we find that we get $(c \Delta c) \Delta (c \Delta c) = x$, which, by line $1$, we know is true.

*From lines $4$ and $5$ we can conclude that there does indeed exist such a value $b$ for which the statement holds.

*From lines $3$ to $6$ we can conclude similarly that there exists such a value $a$.

*From lines $2$ to $7$ we can conclude that this works for all $x$.

*QED


The reason I am skeptical is that I am basically using the statement in the conclusion to conclude itself. Is this allowed?
 A: To prove the given implication you need to show that if the antecedent, $ \forall_{x} \exists_{y} [y \Delta y = x]\ $, is true then the consequent, $\ \forall_{x} \exists_{a} \exists_{b} \left[ (a \Delta a) \Delta b = x \right]\ $, must also be true—that is, given any $\ x\ $ you can find $\ a\ $ and $\ b\ $ such that $\ (a \Delta a) \Delta b = x\ $. The only assumption you're allowed to make in a valid proof is that the antecedent is true—that is, given any $\ x\ $ you can find a $\ y\ $ such that $\ y \Delta y = x\ $.
You're scepticism about the validity of your proposed proof is quite justified.  You start off correctly by assuming the antecedent in step $1$, and choosing an arbitrary $\ x\ $ in step $2$.  However, having chosen an (apparently arbitrary ) $\ c\ $ for the value of $\ a\ $ in step $3$ and then $\ c\Delta c\ $ for the value of $\ b\ $ in step $4$, you have no justification for assuming, as you appear to do in step $5$, that $\ (a\ \Delta a) \Delta b = x\ $ for those chosen values of $\ a\ $ and $\ b\ $.
What you need to do in step $3$ is use your assumption that the antecedent is true to pick some value of $\ y\ $ such that $\ y\Delta y = x\ $, then let $\ b=y\ $, so you have $\ b\Delta b=x\ $. But now, the antecedent also tells you that you can find another value, $\ y_1\ $, say, of $\ y\ $ such that $\ y_1\Delta y_1=b\ $, and putting $\ a=y_1\ $ gives you $\ a\Delta a=b\ $, and hence $\ (a\ \Delta a) \Delta b = x\ $.
