Metamath Proof Explorer


Theorem eqvrelrefrel

Description: An equivalence relation is reflexive. (Contributed by Peter Mazsa, 29-Dec-2021)

Ref Expression
Assertion eqvrelrefrel EqvRel R RefRel R

Proof

Step Hyp Ref Expression
1 df-eqvrel EqvRel R RefRel R SymRel R TrRel R
2 1 simp1bi EqvRel R RefRel R