Theorem errel 7339

Description: An equivalence relation is a relation. (Contributed by Mario Carneiro, 12-Aug-2015.)

Assertion

Ref	Expression
errel

Proof of Theorem errel

Step	Hyp	Ref	Expression
1		df-er 7330	. 2
2	1	simp1bi 1011	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  ersym  7342  ertr  7345  ercnv  7351  erssxp  7353  erth  7375  iiner  7402  frgpuplem  16790  ismntop  28004  topfneec  30173  prter3  30623

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