Theorem erdm 8579

Description: The domain of an equivalence relation. (Contributed by Mario Carneiro, 12-Aug-2015.)

Assertion

Ref	Expression
erdm	⊢ (𝑅 Er 𝐴 → dom 𝑅 = 𝐴)

Proof of Theorem erdm

Step	Hyp	Ref	Expression
1		df-er 8569	. 2 ⊢ (𝑅 Er 𝐴 ↔ (Rel 𝑅 ∧ dom 𝑅 = 𝐴 ∧ (◡𝑅 ∪ (𝑅 ∘ 𝑅)) ⊆ 𝑅))
2	1	simp2bi 1145	1 ⊢ (𝑅 Er 𝐴 → dom 𝑅 = 𝐴)

Syntax hints:   → wi 4   = wceq 1540   ∪ cun 3896   ⊆ wss 3898  ^◡ccnv 5619  dom cdm 5620   ∘ ccom 5624  Rel wrel 5625   Er wer 8566

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 206  df-an 397  df-3an 1088  df-er 8569

This theorem is referenced by:  ercl  8580  erref  8589  errn  8591  erssxp  8592  erexb  8594  ereldm  8617  uniqs2  8639  iiner  8649  eceqoveq  8682  prsrlem1  10929  ltsrpr  10934  0nsr  10936  divsfval  17355  sylow1lem3  19301  sylow1lem5  19303  sylow2a  19320  vitalilem2  24879  vitalilem3  24880  vitalilem5  24882  prjspnn0  40729