Metamath Proof Explorer

Theorem errel

Description: An equivalence relation is a relation. (Contributed by Mario Carneiro, 12-Aug-2015)

Ref Expression
Assertion errel 
|- ( R Er A -> Rel R )

Proof

Step Hyp Ref Expression
1 df-er 
 |-  ( R Er A <-> ( Rel R /\ dom R = A /\ ( `' R u. ( R o. R ) ) C_ R ) )
2 1 simp1bi 
 |-  ( R Er A -> Rel R )