Theorem erdm 8466

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

Syntax hints:   → wi 4   = wceq 1539   ∪ cun 3881   ⊆ wss 3883  ^◡ccnv 5579  dom cdm 5580   ∘ ccom 5584  Rel wrel 5585   Er wer 8453

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 396  df-3an 1087  df-er 8456

This theorem is referenced by:  ercl  8467  erref  8476  errn  8478  erssxp  8479  erexb  8481  ereldm  8504  uniqs2  8526  iiner  8536  eceqoveq  8569  prsrlem1  10759  ltsrpr  10764  0nsr  10766  divsfval  17175  sylow1lem3  19120  sylow1lem5  19122  sylow2a  19139  vitalilem2  24678  vitalilem3  24679  vitalilem5  24681