Need a FOL derivation validated. Unclear on universal generalization restriction. I'm currently working through Suppes' Introduction to Logic, and while the text is excellent, the lack of solutions to the exercises can be frustrating at times.  This is one of those times.  I've racked my brain, but I can't seem to get best whether my solution to a particular exercise is correct or not, and I don't want to move to the next chapter without having a full and complete grasp of the concepts.
The exercise is as follows.  Derive the sentence: 
$(\forall x)(\forall y)(xEy \to yEx)$ 
where $E$ is some 2-place predicate, from the single premise:
$(\forall x)(\forall y)(xEy \longleftrightarrow (\forall z)(xLz \longleftrightarrow yLz) \wedge xLy \wedge yLx)$ where $L$ is some 2-place predicate.
I tried a few different strategies, but got stuck on each one.  In the derivation I'm about to give, it's unclear to me if I've violated a restriction on universal generalization.  Here goes.
1.  $\color{blue}{(\forall x)(\forall y)(xEy \longleftrightarrow (\forall z)(xLz \longleftrightarrow yLz) \wedge xLy \wedge yLx)}$
2.  $\color{blue}{(\alpha E\alpha \longleftrightarrow (\forall z)(\alpha Lz \longleftrightarrow \alpha Lz) \wedge \alpha L\alpha \wedge \alpha L\alpha)}$
3. $\color{blue}{(\alpha E\alpha \to (\forall z)(\alpha Lz \longleftrightarrow \alpha Lz) \wedge \alpha L\alpha \wedge \alpha L\alpha)) \wedge ((\forall z)(\alpha Lz \longleftrightarrow \alpha Lz) \wedge \alpha L\alpha \wedge \alpha L\alpha) \to \alpha E\alpha)}$
4. $\color{blue}{\alpha E\alpha \to (\forall z)(\alpha Lz \longleftrightarrow \alpha Lz) \wedge \alpha L\alpha \wedge \alpha L\alpha}$
5. $\color{blue}{((\forall z)(\alpha Lz \longleftrightarrow \alpha Lz) \wedge \alpha L\alpha \wedge \alpha L\alpha) \to \alpha E\alpha}$
6. $\color{blue}{\alpha E\alpha}$  (here we introduce the antecedent of our desired conclusion as a premise)
7. $\color{blue}{(\forall z)(\alpha Lz \longleftrightarrow \alpha Lz) \wedge \alpha L\alpha \wedge \alpha L\alpha}$
8. $\color{blue}{\alpha E\alpha}$
9. $\color{blue}{\alpha E\alpha \to \alpha E\alpha}$  (here we apply the rule of conditional proof)
10. $\color{blue}{(\forall x)(\forall y)(xEy \to yEx)}$  (valid application of UG?)
For clarity, I'll mention which inference rules are in use here.  We arrive at 2. from 1. by universal specification on both $x$ and $y$ (I chose to use $\alpha$ as the object being instantiated and thus standing-in for $x$ and $y$).  3. is tautologically equivalent to 2..  Lines 4. and 5. come from 2. by applying the Law of Simplification.  Line 6. is where I introduce a new premise.  It should be noted that $\alpha$ is indeed a free variable on this Line 6..  I introduce this line as a premise with the intent of later applying the Rule of Conditional Proof (aka the Deduction Theorem).  We arrive at 7. from lines 4. and 6. by the Law of Detachment.  
(At this point I'm happy because I've been able to make use of my Line-6 premise, and thus have set myself up to be able to later conditionalize on Line-6 and achieve a CP.)
We arrive at 8. from lines 5. and 7. by Detachment as well.  We arrive at line 9. from lines 6. and 8. via Rule CP.  By conditionalizing on our line 6. premise, we should be allowed to apply universal generalization and achieve our desired conclusion, which is done on line 10..
The problem is (in my mind), is that on line 9., there is only a single object shown (the $\alpha$).  Does this mean that I cannot apply UG as I have done on line 10.?  What I've done just doesn't look or feel right.  Yet, I'm not able to see how I've violated any of the constraints associated with the application of universal generalization.  In my mind, what should only be allowed on line 10. is an application of UG like this: $\color{blue}{(\forall x)(xEx \to xEx)}$.  Is my intuition fallacious?  I guess in some sense, what I'm asking here is the converse of this question I asked just yesterday.  I was hoping the answer given in that question would get me through this exercise, but unfortunately I'm stuck once more, this time on UG constraints.
For what it's worth, I didn't bother to do much with the $\color{blue}{(\forall z)(xLz \longleftrightarrow yLz) \wedge xLy \wedge yLx)}$ as I just can't see how it would help me in getting to the conclusion.  
Having said that, I'm relatively confident that my derivation is valid, except for the application of UG on line 10.*  Is there a flaw in this derivation?  Is line **10. a valid application of UG?  If there is a flaw in any of this, any help / guidance would be greatly appreciated.
-Paul
 A: You cannot simultaneously generalize the same constant to two different variables-that is, your intuition about line 9 to line 10 is correct, and the proof won't go through. One presentation of UG is that from $\varphi(\alpha)$ deduce $\forall x \varphi(x)$ as long as
$\alpha$ did not appear in the assumption(s) leading to $\varphi(\alpha)$ and $x$ does not appear free in $\varphi$.
What may be more useful is an example of why this sort of reasoning won't work. To wit, I offer this proof that everything is logically equivalent to everything else:
$$\forall x: \varphi(x)\leftrightarrow \varphi(x)$$
$$\varphi(\alpha)\leftrightarrow \varphi(\alpha)$$
$$\forall x \forall y\ \varphi(x) \leftrightarrow \varphi(y)$$
A: You cannot obtain 10. from 9. by UG. 
From 9., with UG, you will get :

$(∀x)(xEx → xEx)$

which is not what we need.
Basically, your initial steps are right, but without using the same term $\alpha$ in the two applcations of US.
I'll suggest as 2. :

2'. $(x E y \leftrightarrow (∀z)(xLz \leftrightarrow yLz) \land xLy \land yLx)$. 

Then we proceed as 6'. above, assuming $xEy$ and "detaching" :

7'. $(∀z)(xLz \leftrightarrow yLz) \land xLy \land yLx$.

Now we apply US again, to get :

$(xLz \leftrightarrow yLz) \land xLy \land yLx$.

Here we need some "propositional transformations", in order to "rearrange" it as :

$(yLz \leftrightarrow xLz) \land yLx \land xLy$

[Note: I'm not familiar with Suppes' rule-set, by I think that it is not difficult to justify it ...].
Then we apply UG to $z$, which is not free in 1. nor in 6'., to get :

$(\forall z)((yLz \leftrightarrow xLz) \land yLx \land xLy)$

Now we have to start again from 1. After the renaming of the bound variable $y$ [using : $\forall x \forall y \varphi \vdash \forall x \forall w \varphi$, where $w$ is new], we apply again US to $\forall x$ with the term $y$ and then US to $\forall w$ with the term $x$, to get :

5'. $(\forall z)((yLz \leftrightarrow xLz) \land yLx \land xLy) \rightarrow yEx$

and applying Detachement we get :

8'. $yEx$.

Now it is done ! 
From 6'. and 8'., by Conditional Proof, we get :

$xEy \rightarrow yEx$;

and now we apply UG twice (first $y$ and then $x$; both are not free in the unique assumption left, which is 1.) concluding with :


$(\forall x)(\forall y)(xEy \rightarrow yEx)$.


I hope it can help ...
