Theorem erdm 8293

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

Syntax hints:   → wi 4   = wceq 1533   ∪ cun 3933   ⊆ wss 3935  ^◡ccnv 5548  dom cdm 5549   ∘ ccom 5553  Rel wrel 5554   Er wer 8280

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 209  df-an 399  df-3an 1085  df-er 8283

This theorem is referenced by:  ercl  8294  erref  8303  errn  8305  erssxp  8306  erexb  8308  ereldm  8331  uniqs2  8353  iiner  8363  eceqoveq  8396  prsrlem1  10488  ltsrpr  10493  0nsr  10495  divsfval  16814  sylow1lem3  18719  sylow1lem5  18721  sylow2a  18738  vitalilem2  24204  vitalilem3  24205  vitalilem5  24207