Theorem erdm 8654

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

Syntax hints:   → wi 4   = wceq 1542   ∪ cun 3887   ⊆ wss 3889  ^◡ccnv 5630  dom cdm 5631   ∘ ccom 5635  Rel wrel 5636   Er wer 8640

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 8643

This theorem is referenced by:  ercl  8655  erref  8664  errn  8666  erssxp  8667  erexb  8669  ereldm  8697  uniqs2  8723  iiner  8736  eceqoveq  8769  prsrlem1  10995  ltsrpr  11000  0nsr  11002  divsfval  17511  sylow1lem3  19575  sylow1lem5  19577  sylow2a  19594  vitalilem2  25576  vitalilem3  25577  vitalilem5  25579  prjspnn0  43055