Theorem erdm 8681

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

Syntax hints:   → wi 4   = wceq 1540   ∪ cun 3912   ⊆ wss 3914  ^◡ccnv 5637  dom cdm 5638   ∘ ccom 5642  Rel wrel 5643   Er wer 8668

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 8671

This theorem is referenced by:  ercl  8682  erref  8691  errn  8693  erssxp  8694  erexb  8696  ereldm  8724  uniqs2  8750  iiner  8762  eceqoveq  8795  prsrlem1  11025  ltsrpr  11030  0nsr  11032  divsfval  17510  sylow1lem3  19530  sylow1lem5  19532  sylow2a  19549  vitalilem2  25510  vitalilem3  25511  vitalilem5  25513  prjspnn0  42610