Definition df-er 4245

Description: Define the equivalence predicate. R need not be a relation but ordinarily will be, in which case we call it an equivalence relation. Our notation is not standard. A formal notation doesn't seem to exist in the literature; instead only informal English tends to be used. Some definitions in the literature may also require that R be a relation. The present definition, although somewhat cryptic, nicely avoids dummy variables. In dfer2 4246 we derive a more typical definition. We show that an equivalence relation is reflexive, symmetric, and transitive in erref 4259, ersymb 4257, and ertr 4258.

Assertion

Ref	Expression
df-er	|- (Er R <-> (`'R u. (R o. R)) (_ R)

Detailed syntax breakdown of Definition df-er

Step	Hyp	Ref	Expression
1		cR	. . 3 class R
2	1	wer 4242	. 2 wff Er R
3	1	ccnv 3159	. . . 4 class `'R
4	1, 1	ccom 3164	. . . 4 class (R o. R)
5	3, 4	cun 2035	. . 3 class (`'R u. (R o. R))
6	5, 1	wss 2037	. 2 wff (`'R u. (R o. R)) (_ R
7	2, 6	wb 146	1 wff (Er R <-> (`'R u. (R o. R)) (_ R)

This definition is referenced by:  dfer2 4246  ereq 4251

Copyright terms: Public domain