Prove If $\forall x \in X((x,x) \in R)$ then $\forall x \in X \exists y \in X(x,y) \in R$

Question

I have been solving one problem and at the end of the proof after performing some transformations, I have been left with this to prove:

If $\forall x \in X((x,x) \in R)$ then $\forall x \in X \exists y \in X((x,y) \in R)$

Even though I feel the above implication is true, I can't seem to produce a proper proof statement for it. Some of my attempt look like this:

Suppose $\forall x \in X((x,x) \in R)$. Let $x$ be an arbitrary element in $X$ and $y$ be some element in $X$. Then we have to prove that $(x,y) \in R$. We know that for every $x$, $(x,x) \in R$. So clearly $(x,y) \in R$.

But I'm still not satisfied with the above phrasing. Is the proof correct ? Is there a better way to do this?

Answer 1

$(\forall x\in X: (x,x)\in R) \vdash (\forall x\in X\;\exists y\in X: (x,y)\in R)$

The metalogic is simply that: if every element in $X$ is $R$-related to itself, then every element in $X$ is $R$-related to some element in $X$.

More formally, you can go through steps of universal instantiation, existential generalization, universal generalisation.

$\forall x \in X: (x,x)\in R \\ \Downarrow\qquad ({\rm Universal\; Instantiation}) \\ (x,x)\in R \\ \Downarrow \qquad({\rm Existential\;Generalization})\\ \exists y\in X: (x,y)\in R \\ \Downarrow \qquad({\rm Universal\;Generalization}) \\ \forall x\in X\exists y\in X: (x,y)\in R$

Answer 2

I think you have the correct idea. I would however phrase things as follows.

Assume that $\forall x$, we have $(x,x)\in R$. This means that for any $x\in X$, we can produce some $y$ such that $(x,y)\in R$ by selecting $y=x$.