Proofs for Relational Predicate Logic --Difficult Question! I have been working on this problem for four and a half hours and I think I have simply missed something. I need the help of my peers here. The rules I am allowed to use are the Basic Inference rules (MP, MT, HS, Simp, Conj, DS, Add, Dil.), the Replacement Rules (DN, Comm, Assoc, Dup, DeM, BE, Contrap, CE, Exp, Dist.), CP, IP, and EI, UI, EG, UG. 
Here is the problem:


*

*(x)[(∃y)Rxy --> (y)Ryx]

*Rab   /∴ (x)(y)Rxy


My professor gave us the hint to use premise 1 two times. 
I feel very silly because I know I have missed something simple (as usual) but I need a second pair of eyes. Please and thank you for your help.
 A: Your premisses are:
$1.\quad \forall x(\exists yRxy \to \forall yRyx)$
$2. \quad Rab$
Instantiate the first universal  with $a$ (what else?) to get 
$3. \quad \exists yRay \to \forall yRya$
Given a conditional, you always look to see if you can get the antecedent and use modus ponens. And yes! Of course you can. By existential generalization on $b$, (2) gives you the antecedent of (3), so we can use modus ponens to get to
$4. \quad \forall yRya$.
But now where? If we are going to get to a universally quantified conclusion, we know we are going to need to get it from some wff where the only parameters are arbitrary (not a fixed constant like $a$), so we can then generalize on them. So we are going to need something other than $4$. Hmmmm. Ok, let's use the purely general (1) and instantiate  with a new parameter (arbitrary name, free variable, however you like to think of if) $v$. That's just brute force, but what else can we do? It is the only option. That gives us
$5. \quad \exists yRvy \to \forall yRyv$
But aha! Another conditional. Can we get the antecedent? But it is immediate that (4) gives us $Rva$ and hence $\exists yRvy$, so modus ponens again gives us
$6 \quad \forall yRyv$
And now the end is in sight. 
But drat! We can't just quantify that as is (or rather, we can but then n we'd get $\forall x\forall yRyx$  which has things the wrong way around). To get the quantifiers the right way round, we have to take another step. Instantiate (6) with a new parameter $u$ to get
$7 \quad Ruv$.
But $u$ and $v$ were arbitrary, so you can universally quantify twice (do it in the right order!) and you get, lo and behold,
$8 \quad \forall x\forall yRxy$.
[Happily, this is what is sometimes called a "Just Do It" proof -- i.e. at every step you do the only sensible thing, and it all works out fine!]
A: This is a "long" comment about the "equivalence" of the restrictions about UG rule.
In "standard" natural deduction systems, we have that :

in $\forall$-I the variable $x$ may not occur free in any hypothesis on which $\varphi(x)$ depends, i.e. an uncanceled hypothesis [see e.g.Dirk van Dalen, Logic and Structure (5th ed - 2013), page 86].

With this restriction, we can prove, the Lemma :

$\forall x (\varphi(x) \rightarrow \psi(x)) \vdash \forall x \varphi(x) \rightarrow \forall x \psi(x)$

in the following way :
1) $\forall x (\varphi(x) \rightarrow \psi(x))$ --- Assumption
2) $\varphi(a) \rightarrow \psi(a)$ --- $\forall$-E (or UI)
3) $\forall x \varphi(x)$ --- Assumption
4) $\varphi(a)$ --- from 3) by UI
5) $\psi(a)$ --- form 3) and 4) by MP
6) $\forall x \psi(x)$ --- from 5) by $\forall$-I (or UG) : $a$ is not free in the Assumptions
7) $\forall x \varphi(x) \rightarrow \forall x \psi(x)$ --- from 6) by $\rightarrow$-intro, "discharging" the Assumption in 3) (please, check on your textbook : I think it is CP).
Now for the "other way".
I'll refer to Daniel Bonevac, Deduction. Introductory Symbolic Logic (2nd ed - 2003), page 215 for Universal proof (how to prove an universal conclusion) and example page 216, where the restiction is that :

Universal Generalization requires that the variable be completely new to the proof.

We proceed as follows :
1) $\forall x (\varphi(x) \rightarrow \psi(x))$ --- Assumption
2) $\forall x \varphi(x)$ --- Assumption
3) (we want to) show : $\forall x \psi(x)$
4) $| \quad$ to show $\psi(a)$ we assume the constant $a$ new to the proof
5) $| \quad \varphi(a)$ --- from 2) by UI
6) $| \quad \varphi(a) \rightarrow \psi(a)$ --- from 1) by UI 
7) $| \quad \psi(a)$ --- from 6) and 5) by MP
having proved that an arbitrary object $a$ "is $\psi$", we may conclude :
8) $\forall x \psi(x)$ ("crossig" the show).
Finally, we apply $\rightarrow$-intro (or CP) to get :
9) $\forall x \varphi(x) \rightarrow \forall x \psi(x)$, discharging the Assumption 2).
I hope it can help ...
