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

Theorem erdm 7381
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 7371 . 2  |-  ( R  Er  A  <->  ( Rel  R  /\  dom  R  =  A  /\  ( `' R  u.  ( R  o.  R ) ) 
C_  R ) )
21simp2bi 1021 1  |-  ( R  Er  A  ->  dom  R  =  A )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1437    u. cun 3440    C_ wss 3442   `'ccnv 4853   dom cdm 4854    o. ccom 4858   Rel wrel 4859    Er wer 7368
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 188  df-an 372  df-3an 984  df-er 7371
This theorem is referenced by:  ercl  7382  erref  7391  errn  7393  erssxp  7394  erexb  7396  ereldm  7415  uniqs2  7433  iiner  7443  eceqoveq  7476  prsrlem1  9495  ltsrpr  9500  0nsr  9502  divsfval  15404  sylow1lem3  17187  sylow1lem5  17189  sylow2a  17206  vitalilem2  22444  vitalilem3  22445  vitalilem5  22447
  Copyright terms: Public domain W3C validator