Theorem erdm 8710

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 8699	. 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 8696

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 8699

This theorem is used by:  ercl  8711  erref  8720  errn  8722  erssxp  8723  erexb  8725  ereldm  8753  uniqs2  8779  iiner  8792  eceqoveq  8825  prsrlem1  11084  ltsrpr  11089  0nsr  11091  divsfval  17636  sylow1lem3  19730  sylow1lem5  19732  sylow2a  19749  vitalilem2  25840  vitalilem3  25841  vitalilem5  25843  prjspnn0  43471