Theorem erdm 8648

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

Syntax hints:   → wi 4   = wceq 1548   ∪ cun 3883   ⊆ wss 3885  ^◡ccnv 5620  dom cdm 5621   ∘ ccom 5625  Rel wrel 5626   Er wer 8634

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 209  df-an 398  df-3an 1095  df-er 8637

This theorem is referenced by:  ercl  8649  erref  8658  errn  8660  erssxp  8661  erexb  8663  ereldm  8691  uniqs2  8717  iiner  8730  eceqoveq  8763  prsrlem1  10990  ltsrpr  10995  0nsr  10997  divsfval  17506  sylow1lem3  19570  sylow1lem5  19572  sylow2a  19589  vitalilem2  25598  vitalilem3  25599  vitalilem5  25601  prjspnn0  43087