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 )