Theorem erdm 8707

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

Syntax hints:   → wi 4   = wceq 1567   ∪ cun 3911   ⊆ wss 3913  ^◡ccnv 5663  dom cdm 5664   ∘ ccom 5668  Rel wrel 5669   Er wer 8693

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 210  df-an 401  df-3an 1103  df-er 8696

This theorem is referenced by:  ercl  8708  erref  8717  errn  8719  erssxp  8720  erexb  8722  ereldm  8750  uniqs2  8776  iiner  8789  eceqoveq  8822  prsrlem1  11059  ltsrpr  11064  0nsr  11066  divsfval  17603  sylow1lem3  19672  sylow1lem5  19674  sylow2a  19691  vitalilem2  25739  vitalilem3  25740  vitalilem5  25742  prjspnn0  43283