Theorem erdm 8656

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

Syntax hints:   → wi 4   = wceq 1542   ∪ cun 3901   ⊆ wss 3903  ^◡ccnv 5631  dom cdm 5632   ∘ ccom 5636  Rel wrel 5637   Er wer 8642

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 1089  df-er 8645

This theorem is referenced by:  ercl  8657  erref  8666  errn  8668  erssxp  8669  erexb  8671  ereldm  8699  uniqs2  8725  iiner  8738  eceqoveq  8771  prsrlem1  10995  ltsrpr  11000  0nsr  11002  divsfval  17480  sylow1lem3  19541  sylow1lem5  19543  sylow2a  19560  vitalilem2  25578  vitalilem3  25579  vitalilem5  25581  prjspnn0  42980