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 3900   ⊆ wss 3902  ^◡ccnv 5658  dom cdm 5659   ∘ ccom 5663  Rel wrel 5664   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  11082  ltsrpr  11087  0nsr  11089  divsfval  17635  sylow1lem3  19726  sylow1lem5  19728  sylow2a  19745  vitalilem2  25836  vitalilem3  25837  vitalilem5  25839  prjspnn0  43453