Theorem erdm 8684

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

Syntax hints:   → wi 4   = wceq 1540   ∪ cun 3915   ⊆ wss 3917  ^◡ccnv 5640  dom cdm 5641   ∘ ccom 5645  Rel wrel 5646   Er wer 8671

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 8674

This theorem is referenced by:  ercl  8685  erref  8694  errn  8696  erssxp  8697  erexb  8699  ereldm  8727  uniqs2  8753  iiner  8765  eceqoveq  8798  prsrlem1  11032  ltsrpr  11037  0nsr  11039  divsfval  17517  sylow1lem3  19537  sylow1lem5  19539  sylow2a  19556  vitalilem2  25517  vitalilem3  25518  vitalilem5  25520  prjspnn0  42617