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

Theorem erdm 7224
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 7214 . 2  |-  ( R  Er  A  <->  ( Rel  R  /\  dom  R  =  A  /\  ( `' R  u.  ( R  o.  R ) ) 
C_  R ) )
21simp2bi 1004 1  |-  ( R  Er  A  ->  dom  R  =  A )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1370    u. cun 3437    C_ wss 3439   `'ccnv 4950   dom cdm 4951    o. ccom 4955   Rel wrel 4956    Er wer 7211
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 185  df-an 371  df-3an 967  df-er 7214
This theorem is referenced by:  ercl  7225  erref  7234  errn  7236  erssxp  7237  erexb  7239  ereldm  7257  uniqs2  7275  iiner  7285  eceqoveq  7318  th3qlem1  7319  ltsrpr  9358  0nsr  9360  divsfval  14607  sylow1lem3  16223  sylow1lem5  16225  sylow2a  16242  vitalilem2  21225  vitalilem3  21226  vitalilem5  21228
  Copyright terms: Public domain W3C validator