Theorem erdm 8728

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569   ⊆ wss 3895   ∪ cun 4149  ^◡ccnv 5649  dom cdm 5650   ∘ ccom 5654  Rel wrel 5655   Er wer 8714

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 8717

This theorem is used by:  ercl  8729  erref  8738  errn  8740  erssxp  8741  erexb  8743  ereldm  8771  uniqs2  8797  iiner  8810  eceqoveq  8843  prsrlem1  11157  ltsrpr  11162  0nsr  11164  divsfval  17719  sylow1lem3  19814  sylow1lem5  19816  sylow2a  19833  vitalilem2  25930  vitalilem3  25931  vitalilem5  25933  prjspnn0  43652