Theorem erdm 8091

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

Syntax hints:   → wi 4   = wceq 1507   ∪ cun 3823   ⊆ wss 3825  ^◡ccnv 5399  dom cdm 5400   ∘ ccom 5404  Rel wrel 5405   Er wer 8078

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 199  df-an 388  df-3an 1070  df-er 8081

This theorem is referenced by:  ercl  8092  erref  8101  errn  8103  erssxp  8104  erexb  8106  ereldm  8129  uniqs2  8151  iiner  8161  eceqoveq  8194  prsrlem1  10284  ltsrpr  10289  0nsr  10291  divsfval  16666  sylow1lem3  18476  sylow1lem5  18478  sylow2a  18495  vitalilem2  23903  vitalilem3  23904  vitalilem5  23906