Theorem erdm 7752

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

Syntax hints:   → wi 4   = wceq 1483   ∪ cun 3572   ⊆ wss 3574  ^◡ccnv 5113  dom cdm 5114   ∘ ccom 5118  Rel wrel 5119   Er wer 7739

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 197  df-an 386  df-3an 1039  df-er 7742

This theorem is referenced by:  ercl  7753  erref  7762  errn  7764  erssxp  7765  erexb  7767  ereldm  7790  uniqs2  7809  iiner  7819  eceqoveq  7853  prsrlem1  9893  ltsrpr  9898  0nsr  9900  divsfval  16207  sylow1lem3  18015  sylow1lem5  18017  sylow2a  18034  vitalilem2  23378  vitalilem3  23379  vitalilem5  23381