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

Theorem erdm 6670
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 6660 . 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 1623    u. cun 3150    C_ wss 3152   `'ccnv 4688   dom cdm 4689    o. ccom 4693   Rel wrel 4694    Er wer 6657
This theorem is referenced by:  ercl  6671  erref  6680  errn  6682  erssxp  6683  erexb  6685  ereldm  6703  uniqs2  6721  iiner  6731  eceqoveq  6763  th3qlem1  6764  ltsrpr  8699  0nsr  8701  divsfval  13449  sylow1lem3  14911  sylow1lem5  14913  sylow2a  14930  vitalilem2  18964  vitalilem3  18965  vitalilem5  18967
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 6660
  Copyright terms: Public domain W3C validator