ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-er Structured version   Unicode version

Definition df-er 6042
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 6043 we derive a more typical definition. We show that an equivalence relation is reflexive, symmetric, and transitive in erref 6062, ersymb 6056, and ertr 6057. (Contributed by NM, 4-Jun-1995.) (Revised by Mario Carneiro, 2-Nov-2015.)
Assertion
Ref Expression
df-er  R  Er  Rel 
R  dom  R  `' R  u.  R  o.  R 
C_  R

Detailed syntax breakdown of Definition df-er
StepHypRef Expression
1 cA . . 3
2 cR . . 3  R
31, 2wer 6039 . 2  R  Er
42wrel 4293 . . 3  Rel  R
52cdm 4288 . . . 4  dom  R
65, 1wceq 1242 . . 3  dom  R
72ccnv 4287 . . . . 5  `' R
82, 2ccom 4292 . . . . 5  R  o.  R
97, 8cun 2909 . . . 4  `' R  u.  R  o.  R
109, 2wss 2911 . . 3  `' R  u.  R  o.  R  C_  R
114, 6, 10w3a 884 . 2  Rel  R  dom  R  `' R  u.  R  o.  R  C_  R
123, 11wb 98 1  R  Er  Rel 
R  dom  R  `' R  u.  R  o.  R 
C_  R
Colors of variables: wff set class
This definition is referenced by:  dfer2  6043  ereq1  6049  ereq2  6050  errel  6051  erdm  6052  ersym  6054  ertr  6057  xpiderm  6113
  Copyright terms: Public domain W3C validator