Metamath Proof Explorer


Theorem eqvrelrefrel

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

Ref Expression
Assertion eqvrelrefrel ( EqvRel 𝑅 → RefRel 𝑅 )

Proof

Step Hyp Ref Expression
1 df-eqvrel ( EqvRel 𝑅 ↔ ( RefRel 𝑅 ∧ SymRel 𝑅 ∧ TrRel 𝑅 ) )
2 1 simp1bi ( EqvRel 𝑅 → RefRel 𝑅 )