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 we derive a
more typical definition. We show that an equivalence relation is
reflexive, symmetric, and transitive in erref , ersymb , and ertr .
(Contributed by NM, 4-Jun-1995)(Revised by Mario Carneiro, 2-Nov-2015)