Theorem erdm 8713

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

Syntax hints:   → wi 4   = wceq 1542   ∪ cun 3947   ⊆ wss 3949  ^◡ccnv 5676  dom cdm 5677   ∘ ccom 5681  Rel wrel 5682   Er wer 8700

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 398  df-3an 1090  df-er 8703

This theorem is referenced by:  ercl  8714  erref  8723  errn  8725  erssxp  8726  erexb  8728  ereldm  8751  uniqs2  8773  iiner  8783  eceqoveq  8816  prsrlem1  11067  ltsrpr  11072  0nsr  11074  divsfval  17493  sylow1lem3  19468  sylow1lem5  19470  sylow2a  19487  vitalilem2  25126  vitalilem3  25127  vitalilem5  25129  prjspnn0  41364