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

Theorem erdm 7907
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 7897 . 2 (𝑅 Er 𝐴 ↔ (Rel 𝑅 ∧ dom 𝑅 = 𝐴 ∧ (𝑅 ∪ (𝑅𝑅)) ⊆ 𝑅))
21simp2bi 1140 1 (𝑅 Er 𝐴 → dom 𝑅 = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1631  cun 3722  wss 3724  ccnv 5249  dom cdm 5250  ccom 5254  Rel wrel 5255   Er wer 7894
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 383  df-3an 1073  df-er 7897
This theorem is referenced by:  ercl  7908  erref  7917  errn  7919  erssxp  7920  erexb  7922  ereldm  7943  uniqs2  7962  iiner  7972  eceqoveq  8006  prsrlem1  10096  ltsrpr  10101  0nsr  10103  divsfval  16416  sylow1lem3  18223  sylow1lem5  18225  sylow2a  18242  vitalilem2  23598  vitalilem3  23599  vitalilem5  23601
  Copyright terms: Public domain W3C validator