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

Theorem erdm 8755
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 8745 . 2 (𝑅 Er 𝐴 ↔ (Rel 𝑅 ∧ dom 𝑅 = 𝐴 ∧ (𝑅 ∪ (𝑅𝑅)) ⊆ 𝑅))
21simp2bi 1147 1 (𝑅 Er 𝐴 → dom 𝑅 = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1540  cun 3949  wss 3951  ccnv 5684  dom cdm 5685  ccom 5689  Rel wrel 5690   Er wer 8742
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 207  df-an 396  df-3an 1089  df-er 8745
This theorem is referenced by:  ercl  8756  erref  8765  errn  8767  erssxp  8768  erexb  8770  ereldm  8795  uniqs2  8819  iiner  8829  eceqoveq  8862  prsrlem1  11112  ltsrpr  11117  0nsr  11119  divsfval  17592  sylow1lem3  19618  sylow1lem5  19620  sylow2a  19637  vitalilem2  25644  vitalilem3  25645  vitalilem5  25647  prjspnn0  42632
  Copyright terms: Public domain W3C validator