Help with a simple proof in predicate logic (with identity) it's been a while since I've done formal logic, and I was trying to help a friend with a proof. His logic course is using Lemmon's Beginning Logic. Here's what he's supposed to show, without using reductio ad absurdum:
$$\exists x\,\forall y\,Ryx \vdash \exists y\,\forall x\quad x=y \implies \forall z\, Rzx.$$
Intuitively, the premise could be understood to say there's someone who is $R$'ed (e.g. respected) by everyone. And the conclusion could be understood to say there's someone such that anyone who turns out to be the very same individual is $R$'ed by everyone. So it seems like the conclusion is just a convoluted way of restating the premise. But I'll be damned if I know how to get started with the proof.
 A: I'm not familiar with Lemmon's proof system, but I'll give you a Natural Deduction derivation.
The key step is the equality rule $(=\text E)$ [see Ian Chiswell & Wilfrid Hodges, Mathematical Logic (2007), page 122]:

$$\dfrac{(s=t) \ \ \ \ \ \ \phi[s/x]}{\phi[t/x]}$$

Thus, from the premise :
1) $∃x∀yRyx$
we need the temporary assumption :
2) $∀yRya$ --- [a],
and then we apply a "standard" sub-derivation to rename the bound variable $x$, getting:
3) $∀zRza$.
Now we apply the rule $(=\text E)$ in the form : $(a=x), \ ∀zRza \vdash ∀zRzx$ [with $∀zRzw$ as  $\phi(w)$] with 3) to derive :
4) $(a=x) \vdash ∀zRzx$.
With the "derived rule" $(=\text{symm})$ : $(s=t) \vdash (t=s)$ [see page 123]
followed by $\to$-intro, we get :
5) $(x=a) \to ∀zRzx$.
Now we apply $\forall \text I$ :
6) $\forall x \ [(x=a) \to ∀zRzx]$
followed by $\exists \text I$ :
7) $\exists y \forall x \ [(x=y) \to ∀zRzx]$.
All the derivation is "subject" to the assumption [a]. But $a$ is not free in the conclusion 7) of the sub-derivation; thus, we can apply $\exists\text{E}$ : 

$$\dfrac{∃x \phi(x) \ \ \ \ \ \ \phi[t/x] \vdash \psi}{\psi}$$

provided that the term $t$ does not occur in $\psi, \phi$ or any undischarged assumption except $\phi[t/x]$, to 1), 2) and 7) to discharge [a] and conclude with :


$∃x∀yRyx \vdash \exists y \forall x \ [(x=y) \to ∀zRzx]$.


