Theorem erdm 8754

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

Syntax hints:   → wi 4   = wceq 1537   ∪ cun 3961   ⊆ wss 3963  ^◡ccnv 5688  dom cdm 5689   ∘ ccom 5693  Rel wrel 5694   Er wer 8741

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 8744

This theorem is referenced by:  ercl  8755  erref  8764  errn  8766  erssxp  8767  erexb  8769  ereldm  8794  uniqs2  8818  iiner  8828  eceqoveq  8861  prsrlem1  11110  ltsrpr  11115  0nsr  11117  divsfval  17594  sylow1lem3  19633  sylow1lem5  19635  sylow2a  19652  vitalilem2  25658  vitalilem3  25659  vitalilem5  25661  prjspnn0  42609