Definition df-er 4261

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 4262 we derive a more typical definition. We show that an equivalence relation is reflexive, symmetric, and transitive in erref 4275, ersymb 4273, and ertr 4274.

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 4258	. 2 wff Er R
3	1	ccnv 3169	. . . 4 class `'R
4	1, 1	ccom 3174	. . . 4 class (R o. R)
5	3, 4	cun 2045	. . 3 class (`'R u. (R o. R))
6	5, 1	wss 2047	. 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 4262  ereq 4267

Copyright terms: Public domain