Theorem erdm 8401

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

Syntax hints:   → wi 4   = wceq 1543   ∪ cun 3864   ⊆ wss 3866  ^◡ccnv 5550  dom cdm 5551   ∘ ccom 5555  Rel wrel 5556   Er wer 8388

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 210  df-an 400  df-3an 1091  df-er 8391

This theorem is referenced by:  ercl  8402  erref  8411  errn  8413  erssxp  8414  erexb  8416  ereldm  8439  uniqs2  8461  iiner  8471  eceqoveq  8504  prsrlem1  10686  ltsrpr  10691  0nsr  10693  divsfval  17052  sylow1lem3  18989  sylow1lem5  18991  sylow2a  19008  vitalilem2  24506  vitalilem3  24507  vitalilem5  24509