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

Theorem erdm 7313
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 7303 . 2  |-  ( R  Er  A  <->  ( Rel  R  /\  dom  R  =  A  /\  ( `' R  u.  ( R  o.  R ) ) 
C_  R ) )
21simp2bi 1010 1  |-  ( R  Er  A  ->  dom  R  =  A )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1398    u. cun 3459    C_ wss 3461   `'ccnv 4987   dom cdm 4988    o. ccom 4992   Rel wrel 4993    Er wer 7300
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 369  df-3an 973  df-er 7303
This theorem is referenced by:  ercl  7314  erref  7323  errn  7325  erssxp  7326  erexb  7328  ereldm  7347  uniqs2  7365  iiner  7375  eceqoveq  7408  prsrlem1  9438  ltsrpr  9443  0nsr  9445  divsfval  15039  sylow1lem3  16822  sylow1lem5  16824  sylow2a  16841  vitalilem2  22187  vitalilem3  22188  vitalilem5  22190
  Copyright terms: Public domain W3C validator