Metamath Proof Explorer

Theorem eqvrelrel

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

Ref Expression
Assertion eqvrelrel 
|- ( EqvRel R -> Rel R )

Proof

Step Hyp Ref Expression
1 dfeqvrel2 
 |-  ( EqvRel R <-> ( ( ( _I |` dom R ) C_ R /\ `' R C_ R /\ ( R o. R ) C_ R ) /\ Rel R ) )
2 1 simprbi 
 |-  ( EqvRel R -> Rel R )