Theorem erdm 8665

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

Syntax hints:   → wi 4   = wceq 1541   ∪ cun 3911   ⊆ wss 3913  ^◡ccnv 5637  dom cdm 5638   ∘ ccom 5642  Rel wrel 5643   Er wer 8652

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 206  df-an 397  df-3an 1089  df-er 8655

This theorem is referenced by:  ercl  8666  erref  8675  errn  8677  erssxp  8678  erexb  8680  ereldm  8703  uniqs2  8725  iiner  8735  eceqoveq  8768  prsrlem1  11017  ltsrpr  11022  0nsr  11024  divsfval  17443  sylow1lem3  19396  sylow1lem5  19398  sylow2a  19415  vitalilem2  25010  vitalilem3  25011  vitalilem5  25013  prjspnn0  41018