Predicate natural deduction: Prove (∀x R(x,x)) => ∀x∃y R(x,y)

Question

Prove that if the relation R is reflexive, it is also serial:

$ \forall x \space R(x,x) \vdash \forall x \exists y \space R(x,y)$

I've tried this so far but can't think of anything further:

$1. \space \forall x R(x,x) \space\space\space\space\space premise \\ 2. \space R(x0,x0) \space\space\space\space\space \forall x-elimination, \space from \space line \space 1 \\3. \space ... $

Answer 1

Starting from

1. $\forall x R(x,x)$,

apply $\forall$-elimination:

2. $R(x_0, x_0)$

Then $\exists$-introduction. (The trick is to only use the second $x_0$: we're starting from $R(x_0, x_0)$ which is equal to $R(x_0,t) [t := x_0]$.)

3. $\exists y R(x_0,y)$

Finally apply $\forall$-introduction:

4. $\forall x \exists y R(x,y)$.