MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  erdm Unicode version

Theorem erdm 6686
Description: The domain of an equivalence relation. (Contributed by Mario Carneiro, 12-Aug-2015.)
Assertion
Ref Expression
erdm  |-  ( R  Er  A  ->  dom  R  =  A )

Proof of Theorem erdm
StepHypRef Expression
1 df-er 6676 . 2  |-  ( R  Er  A  <->  ( Rel  R  /\  dom  R  =  A  /\  ( `' R  u.  ( R  o.  R ) ) 
C_  R ) )
21simp2bi 971 1  |-  ( R  Er  A  ->  dom  R  =  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1632    u. cun 3163    C_ wss 3165   `'ccnv 4704   dom cdm 4705    o. ccom 4709   Rel wrel 4710    Er wer 6673
This theorem is referenced by:  ercl  6687  erref  6696  errn  6698  erssxp  6699  erexb  6701  ereldm  6719  uniqs2  6737  iiner  6747  eceqoveq  6779  th3qlem1  6780  ltsrpr  8715  0nsr  8717  divsfval  13465  sylow1lem3  14927  sylow1lem5  14929  sylow2a  14946  vitalilem2  18980  vitalilem3  18981  vitalilem5  18983
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360  df-3an 936  df-er 6676
  Copyright terms: Public domain W3C validator