Metamath Proof Explorer


Theorem eqvrelrel

Description: An equivalence relation is a relation. (Contributed by Peter Mazsa, 2-Jun-2019)

Ref Expression
Assertion eqvrelrel ( EqvRel 𝑅 → Rel 𝑅 )

Proof

Step Hyp Ref Expression
1 dfeqvrel2 ( EqvRel 𝑅 ↔ ( ( ( I ↾ dom 𝑅 ) ⊆ 𝑅 𝑅𝑅 ∧ ( 𝑅𝑅 ) ⊆ 𝑅 ) ∧ Rel 𝑅 ) )
2 1 simprbi ( EqvRel 𝑅 → Rel 𝑅 )