Theorem erdm 8643

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

Syntax hints:   → wi 4   = wceq 1541   ∪ cun 3897   ⊆ wss 3899  ^◡ccnv 5621  dom cdm 5622   ∘ ccom 5626  Rel wrel 5627   Er wer 8630

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 8633

This theorem is referenced by:  ercl  8644  erref  8653  errn  8655  erssxp  8656  erexb  8658  ereldm  8686  uniqs2  8712  iiner  8724  eceqoveq  8757  prsrlem1  10981  ltsrpr  10986  0nsr  10988  divsfval  17466  sylow1lem3  19527  sylow1lem5  19529  sylow2a  19546  vitalilem2  25564  vitalilem3  25565  vitalilem5  25567  prjspnn0  42807