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

Theorem erdm 8300
 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 8290 . 2 (𝑅 Er 𝐴 ↔ (Rel 𝑅 ∧ dom 𝑅 = 𝐴 ∧ (𝑅 ∪ (𝑅𝑅)) ⊆ 𝑅))
21simp2bi 1143 1 (𝑅 Er 𝐴 → dom 𝑅 = 𝐴)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   = wceq 1538   ∪ cun 3881   ⊆ wss 3883  ◡ccnv 5522  dom cdm 5523   ∘ ccom 5527  Rel wrel 5528   Er wer 8287 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 210  df-an 400  df-3an 1086  df-er 8290 This theorem is referenced by:  ercl  8301  erref  8310  errn  8312  erssxp  8313  erexb  8315  ereldm  8338  uniqs2  8360  iiner  8370  eceqoveq  8403  prsrlem1  10501  ltsrpr  10506  0nsr  10508  divsfval  16832  sylow1lem3  18738  sylow1lem5  18740  sylow2a  18757  vitalilem2  24254  vitalilem3  24255  vitalilem5  24257
 Copyright terms: Public domain W3C validator