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

Theorem erdm 6915
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 6905 . 2  |-  ( R  Er  A  <->  ( Rel  R  /\  dom  R  =  A  /\  ( `' R  u.  ( R  o.  R ) ) 
C_  R ) )
21simp2bi 973 1  |-  ( R  Er  A  ->  dom  R  =  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1652    u. cun 3318    C_ wss 3320   `'ccnv 4877   dom cdm 4878    o. ccom 4882   Rel wrel 4883    Er wer 6902
This theorem is referenced by:  ercl  6916  erref  6925  errn  6927  erssxp  6928  erexb  6930  ereldm  6948  uniqs2  6966  iiner  6976  eceqoveq  7009  th3qlem1  7010  ltsrpr  8952  0nsr  8954  divsfval  13772  sylow1lem3  15234  sylow1lem5  15236  sylow2a  15253  vitalilem2  19501  vitalilem3  19502  vitalilem5  19504
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 178  df-an 361  df-3an 938  df-er 6905
  Copyright terms: Public domain W3C validator