Theorem erdm 8658

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

Syntax hints:   → wi 4   = wceq 1540   ∪ cun 3909   ⊆ wss 3911  ^◡ccnv 5630  dom cdm 5631   ∘ ccom 5635  Rel wrel 5636   Er wer 8645

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 8648

This theorem is referenced by:  ercl  8659  erref  8668  errn  8670  erssxp  8671  erexb  8673  ereldm  8701  uniqs2  8727  iiner  8739  eceqoveq  8772  prsrlem1  11001  ltsrpr  11006  0nsr  11008  divsfval  17486  sylow1lem3  19514  sylow1lem5  19516  sylow2a  19533  vitalilem2  25543  vitalilem3  25544  vitalilem5  25546  prjspnn0  42603