Theorem erdm 8753

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ⊆ wss 3900   ∪ cun 4152  ^◡ccnv 5654  dom cdm 5655   ∘ ccom 5659  Rel wrel 5660   Er wer 8739

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105  df-er 8742

This theorem is used by:  ercl  8754  erref  8763  errn  8765  erssxp  8766  erexb  8768  ereldm  8796  uniqs2  8822  iiner  8835  eceqoveq  8868  prsrlem1  11181  ltsrpr  11186  0nsr  11188  divsfval  17745  sylow1lem3  19841  sylow1lem5  19843  sylow2a  19860  vitalilem2  25957  vitalilem3  25958  vitalilem5  25960  ecscottd  35843  prjspnn0  43842