Theorem erdm 8755

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

Syntax hints:   → wi 4   = wceq 1540   ∪ cun 3949   ⊆ wss 3951  ^◡ccnv 5684  dom cdm 5685   ∘ ccom 5689  Rel wrel 5690   Er wer 8742

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 8745

This theorem is referenced by:  ercl  8756  erref  8765  errn  8767  erssxp  8768  erexb  8770  ereldm  8795  uniqs2  8819  iiner  8829  eceqoveq  8862  prsrlem1  11112  ltsrpr  11117  0nsr  11119  divsfval  17592  sylow1lem3  19618  sylow1lem5  19620  sylow2a  19637  vitalilem2  25644  vitalilem3  25645  vitalilem5  25647  prjspnn0  42632