Theorem erdm 8635

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

Syntax hints:   → wi 4   = wceq 1540   ∪ cun 3901   ⊆ wss 3903  ^◡ccnv 5618  dom cdm 5619   ∘ ccom 5623  Rel wrel 5624   Er wer 8622

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 8625

This theorem is referenced by:  ercl  8636  erref  8645  errn  8647  erssxp  8648  erexb  8650  ereldm  8678  uniqs2  8704  iiner  8716  eceqoveq  8749  prsrlem1  10966  ltsrpr  10971  0nsr  10973  divsfval  17451  sylow1lem3  19479  sylow1lem5  19481  sylow2a  19498  vitalilem2  25508  vitalilem3  25509  vitalilem5  25511  prjspnn0  42605