Theorem erdm 8714

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

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

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 8703

This theorem is used by:  ercl  8715  erref  8724  errn  8726  erssxp  8727  erexb  8729  ereldm  8757  uniqs2  8783  iiner  8796  eceqoveq  8829  prsrlem1  11106  ltsrpr  11111  0nsr  11113  divsfval  17658  sylow1lem3  19753  sylow1lem5  19755  sylow2a  19772  vitalilem2  25869  vitalilem3  25870  vitalilem5  25872  prjspnn0  43533