Theorem erdm 8508

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

Syntax hints:   → wi 4   = wceq 1539   ∪ cun 3885   ⊆ wss 3887  ^◡ccnv 5588  dom cdm 5589   ∘ ccom 5593  Rel wrel 5594   Er wer 8495

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 1088  df-er 8498

This theorem is referenced by:  ercl  8509  erref  8518  errn  8520  erssxp  8521  erexb  8523  ereldm  8546  uniqs2  8568  iiner  8578  eceqoveq  8611  prsrlem1  10828  ltsrpr  10833  0nsr  10835  divsfval  17258  sylow1lem3  19205  sylow1lem5  19207  sylow2a  19224  vitalilem2  24773  vitalilem3  24774  vitalilem5  24776