Theorem erdm 8645

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

Syntax hints:   → wi 4   = wceq 1541   ∪ cun 3899   ⊆ wss 3901  ^◡ccnv 5623  dom cdm 5624   ∘ ccom 5628  Rel wrel 5629   Er wer 8632

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 8635

This theorem is referenced by:  ercl  8646  erref  8655  errn  8657  erssxp  8658  erexb  8660  ereldm  8688  uniqs2  8714  iiner  8726  eceqoveq  8759  prsrlem1  10983  ltsrpr  10988  0nsr  10990  divsfval  17468  sylow1lem3  19529  sylow1lem5  19531  sylow2a  19548  vitalilem2  25566  vitalilem3  25567  vitalilem5  25569  prjspnn0  42875