Theorem erdm 8691

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

Syntax hints:   → wi 4   = wceq 1562   ∪ cun 3904   ⊆ wss 3906  ^◡ccnv 5648  dom cdm 5649   ∘ ccom 5653  Rel wrel 5654   Er wer 8677

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 209  df-an 400  df-3an 1101  df-er 8680

This theorem is referenced by:  ercl  8692  erref  8701  errn  8703  erssxp  8704  erexb  8706  ereldm  8734  uniqs2  8760  iiner  8773  eceqoveq  8806  prsrlem1  11032  ltsrpr  11037  0nsr  11039  divsfval  17579  sylow1lem3  19642  sylow1lem5  19644  sylow2a  19661  vitalilem2  25673  vitalilem3  25674  vitalilem5  25676  prjspnn0  43209