Theorem erdm 8632

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

Syntax hints:   → wi 4   = wceq 1541   ∪ cun 3895   ⊆ wss 3897  ^◡ccnv 5613  dom cdm 5614   ∘ ccom 5618  Rel wrel 5619   Er wer 8619

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 207  df-an 396  df-3an 1088  df-er 8622

This theorem is referenced by:  ercl  8633  erref  8642  errn  8644  erssxp  8645  erexb  8647  ereldm  8675  uniqs2  8701  iiner  8713  eceqoveq  8746  prsrlem1  10963  ltsrpr  10968  0nsr  10970  divsfval  17451  sylow1lem3  19512  sylow1lem5  19514  sylow2a  19531  vitalilem2  25537  vitalilem3  25538  vitalilem5  25540  prjspnn0  42725