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

Theorem erdm 7697
Description: The domain of an equivalence relation. (Contributed by Mario Carneiro, 12-Aug-2015.)
Assertion
Ref Expression
erdm (𝑅 Er 𝐴 → dom 𝑅 = 𝐴)

Proof of Theorem erdm
StepHypRef Expression
1 df-er 7687 . 2 (𝑅 Er 𝐴 ↔ (Rel 𝑅 ∧ dom 𝑅 = 𝐴 ∧ (𝑅 ∪ (𝑅𝑅)) ⊆ 𝑅))
21simp2bi 1075 1 (𝑅 Er 𝐴 → dom 𝑅 = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1480  cun 3553  wss 3555  ccnv 5073  dom cdm 5074  ccom 5078  Rel wrel 5079   Er wer 7684
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 197  df-an 386  df-3an 1038  df-er 7687
This theorem is referenced by:  ercl  7698  erref  7707  errn  7709  erssxp  7710  erexb  7712  ereldm  7735  uniqs2  7754  iiner  7764  eceqoveq  7798  prsrlem1  9837  ltsrpr  9842  0nsr  9844  divsfval  16128  sylow1lem3  17936  sylow1lem5  17938  sylow2a  17955  vitalilem2  23284  vitalilem3  23285  vitalilem5  23287
  Copyright terms: Public domain W3C validator