Theorem erdm 8701

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∪ cun 3903   ⊆ wss 3905  ^◡ccnv 5660  dom cdm 5661   ∘ ccom 5665  Rel wrel 5666   Er wer 8687

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 401  df-3an 1105  df-er 8690

This theorem is used by:  ercl  8702  erref  8711  errn  8713  erssxp  8714  erexb  8716  ereldm  8744  uniqs2  8770  iiner  8783  eceqoveq  8816  prsrlem1  11061  ltsrpr  11066  0nsr  11068  divsfval  17605  sylow1lem3  19674  sylow1lem5  19676  sylow2a  19693  vitalilem2  25777  vitalilem3  25778  vitalilem5  25780  prjspnn0  43382