Metamath Proof Explorer

Theorem erdm

Description: The domain of an equivalence relation. (Contributed by Mario Carneiro, 12-Aug-2015)

Ref Expression
Assertion erdm 
|- ( R Er A -> dom R = A )

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 simp2bi 
 |-  ( R Er A -> dom R = A )