Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-er Structured version   Visualization version   Unicode version

Definition df-er 7381
 Description: Define the equivalence relation predicate. Our notation is not standard. A formal notation doesn't seem to exist in the literature; instead only informal English tends to be used. The present definition, although somewhat cryptic, nicely avoids dummy variables. In dfer2 7382 we derive a more typical definition. We show that an equivalence relation is reflexive, symmetric, and transitive in erref 7401, ersymb 7395, and ertr 7396. (Contributed by NM, 4-Jun-1995.) (Revised by Mario Carneiro, 2-Nov-2015.)
Assertion
Ref Expression
df-er

Detailed syntax breakdown of Definition df-er
StepHypRef Expression
1 cA . . 3
2 cR . . 3
31, 2wer 7378 . 2
42wrel 4844 . . 3
52cdm 4839 . . . 4
65, 1wceq 1452 . . 3
72ccnv 4838 . . . . 5
82, 2ccom 4843 . . . . 5
97, 8cun 3388 . . . 4
109, 2wss 3390 . . 3
114, 6, 10w3a 1007 . 2
123, 11wb 189 1
 Colors of variables: wff setvar class This definition is referenced by:  dfer2  7382  ereq1  7388  ereq2  7389  errel  7390  erdm  7391  ersym  7393  ertr  7396  xpider  7452  fcoinver  28290
 Copyright terms: Public domain W3C validator