Theorem erdm 8648

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

Syntax hints:   → wi 4   = wceq 1542   ∪ cun 3888   ⊆ wss 3890  ^◡ccnv 5624  dom cdm 5625   ∘ ccom 5629  Rel wrel 5630   Er wer 8634

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 1089  df-er 8637

This theorem is referenced by:  ercl  8649  erref  8658  errn  8660  erssxp  8661  erexb  8663  ereldm  8691  uniqs2  8717  iiner  8730  eceqoveq  8763  prsrlem1  10989  ltsrpr  10994  0nsr  10996  divsfval  17505  sylow1lem3  19569  sylow1lem5  19571  sylow2a  19588  vitalilem2  25589  vitalilem3  25590  vitalilem5  25592  prjspnn0  43072