Theorem erdm 8773

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 8763	. 2 ⊢ (𝑅 Er 𝐴 ↔ (Rel 𝑅 ∧ dom 𝑅 = 𝐴 ∧ (◡𝑅 ∪ (𝑅 ∘ 𝑅)) ⊆ 𝑅))
2	1	simp2bi 1146	1 ⊢ (𝑅 Er 𝐴 → dom 𝑅 = 𝐴)

Syntax hints:   → wi 4   = wceq 1537   ∪ cun 3974   ⊆ wss 3976  ^◡ccnv 5699  dom cdm 5700   ∘ ccom 5704  Rel wrel 5705   Er wer 8760

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 8763

This theorem is referenced by:  ercl  8774  erref  8783  errn  8785  erssxp  8786  erexb  8788  ereldm  8813  uniqs2  8837  iiner  8847  eceqoveq  8880  prsrlem1  11141  ltsrpr  11146  0nsr  11148  divsfval  17607  sylow1lem3  19642  sylow1lem5  19644  sylow2a  19661  vitalilem2  25663  vitalilem3  25664  vitalilem5  25666  prjspnn0  42577