Theorem erdm 7639

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

Syntax hints:   → wi 4   = wceq 1475   ∪ cun 3538   ⊆ wss 3540  ^◡ccnv 5037  dom cdm 5038   ∘ ccom 5042  Rel wrel 5043   Er wer 7626

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 196  df-an 385  df-3an 1033  df-er 7629

This theorem is referenced by:  ercl  7640  erref  7649  errn  7651  erssxp  7652  erexb  7654  ereldm  7677  uniqs2  7696  iiner  7706  eceqoveq  7740  prsrlem1  9772  ltsrpr  9777  0nsr  9779  divsfval  16030  sylow1lem3  17838  sylow1lem5  17840  sylow2a  17857  vitalilem2  23184  vitalilem3  23185  vitalilem5  23187