Can I justify removing a universal quantifier in this proof? I am trying to prove that the connex property implies reflexivity. 
$\vdash (\forall x,\forall y :  (xRy \lor yRx)) \Rightarrow (\forall x : xRx)$
Here is my attempt
\begin{align*}
    &~~~~~(1)~~(\forall x,\forall y :  (xRy \lor yRx))\\ 
    &~~~~~~~~~~~\text{\{Justification ?? \}} \\
    &\Rightarrow(2)~~(\forall x :  (xRx \lor xRx)) \\
    &~~~~~~~~~~~\text{\{ Idempotency of disjunction in (2) \}}\\   
    &\equiv (3)\forall x : (x R x)\\
  \end{align*}
I am stuck for a justification between steps (1) and (2). The step seems intuitively valid. Do I need a sub-proof or is there some general rule that permits this step?
 A: Your error is that you're trying to prove that the conclusion is equivalent to the premise, whereas you're actually just asked to prove that it follows from the premise.
In a typical formal proof system (here natural deduction) this can be done by almost what you're doing, except without the spurious $\equiv$ signs.


*

*Assume $\forall x \forall y (xRy \lor yRx)$.

*Universal instantiation, setting $x=x$, gives $\forall y (xRy \lor yRx)$.

*Universal instantiation, setting $y=x$, gives $xRx\lor xRx$.

*Propositional equivalece gives $xRx$.

*Universal generalization gives $\forall x(xRx)$.

*Discharge the assumption from step 1, giving $\forall x\forall y (xRy\lor yRx)\to \forall x(xRx)$.

A: You can't justify the passage from $(1)$ to $(2)$. Let $R$ be the equality relation in a set with more than one element. Then $(1)$ is false (that is, there are distinct elements), whereas $(2)$ holds (each element is equal to itself).
Going from $(2)$ to $(3)$ is correct, since $P\vee P\iff P$.
A: $\def\fitch#1#2{~~\begin{array}{|l} #1\\\hline #2 \end{array}}\def\R{\operatorname{R}}$The justification is that: if a predicate is true for any $(x,y)$, then it is true for any $(x,x)$.
Should idempotence be a theorem you may use that; alternatively it may quickly be proven with disjunction elimination.
$$\fitch{}{\fitch{\forall x\forall y:x\R y\vee y\R x }{\fitch{[a]}{\forall y:a\R y\vee y\R a\\a\R a\vee a\R a\\\fitch{a\R a}{}\\a\R a\to a\R a\\a\R a}\\\forall x: x\R x} &\raise{12ex}{\textsf{Assumption}\\[0.5ex] \textsf{Arbitrary Witness}\\[0.5ex]\textsf{Universal Elimination}\\[0.75ex]\textsf{Universal Elimination}\\[0.75ex]\textsf{Assumption}\\[1ex]\textsf{Conditional Introduction}\\[1ex]\textsf{Disjunction Elimination}\\[2ex]\textsf{Universal Introduction}}\\ (\forall x\forall y:x\R y\vee y\R x)\to(\forall x:x\R x)& \textsf{Conditional Introduction}}$$
A: Your attempt fails, because you try to prove the equality, not implication.
$$\forall x\in X \forall y\in X :(xRy \vee yRx)$$
$$\Rightarrow \forall x\in X \exists y=x\in X :(xRy \vee yRx)$$
$$\Rightarrow \forall x\in X  :(xRx \vee xRx)$$
$$\Rightarrow \forall x\in X  :(xRx )$$
