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

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

Detailed syntax breakdown of Definition df-er
StepHypRef Expression
1 cA . . 3  class  A
2 cR . . 3  class  R
31, 2wer 6133 . 2  wff  R  Er  A
42wrel 4377 . . 3  wff  Rel  R
52cdm 4372 . . . 4  class  dom  R
65, 1wceq 1259 . . 3  wff  dom  R  =  A
72ccnv 4371 . . . . 5  class  `' R
82, 2ccom 4376 . . . . 5  class  ( R  o.  R )
97, 8cun 2942 . . . 4  class  ( `' R  u.  ( R  o.  R ) )
109, 2wss 2944 . . 3  wff  ( `' R  u.  ( R  o.  R ) ) 
C_  R
114, 6, 10w3a 896 . 2  wff  ( Rel 
R  /\  dom  R  =  A  /\  ( `' R  u.  ( R  o.  R ) ) 
C_  R )
123, 11wb 102 1  wff  ( R  Er  A  <->  ( Rel  R  /\  dom  R  =  A  /\  ( `' R  u.  ( R  o.  R ) ) 
C_  R ) )
Colors of variables: wff set class
This definition is referenced by:  dfer2  6137  ereq1  6143  ereq2  6144  errel  6145  erdm  6146  ersym  6148  ertr  6151  xpiderm  6207
  Copyright terms: Public domain W3C validator