Theorem erdm 7340

Description: The domain of an equivalence relation. (Contributed by Mario Carneiro, 12-Aug-2015.)

Assertion

Ref	Expression
erdm

Proof of Theorem erdm

Step	Hyp	Ref	Expression
1		df-er 7330	. 2
2	1	simp2bi 1012	1

Syntax hints:  ->wi 4  =wceq 1395  u.cun 3473  C_wss 3475  `'ccnv 5003  domcdm 5004  o.ccom 5008  Relwrel 5009  Erwer 7327

This theorem is referenced by:  ercl  7341  erref  7350  errn  7352  erssxp  7353  erexb  7355  ereldm  7374  uniqs2  7392  iiner  7402  eceqoveq  7435  prsrlem1  9470  ltsrpr  9475  0nsr  9477  divsfval  14944  sylow1lem3  16620  sylow1lem5  16622  sylow2a  16639  vitalilem2  22018  vitalilem3  22019  vitalilem5  22021

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 185  df-an 371  df-3an 975  df-er 7330