Theorem erdm 8638

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

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

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 8628

This theorem is referenced by:  ercl  8639  erref  8648  errn  8650  erssxp  8651  erexb  8653  ereldm  8681  uniqs2  8707  iiner  8719  eceqoveq  8752  prsrlem1  10969  ltsrpr  10974  0nsr  10976  divsfval  17457  sylow1lem3  19518  sylow1lem5  19520  sylow2a  19537  vitalilem2  25543  vitalilem3  25544  vitalilem5  25546  prjspnn0  42721