Definition df-er 3200

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 er2 3201 we derive a more typical definition. We show that an equivalence relation is reflexive, symmetric, and transitive in erref 3212, ersymb 3210, and ertr 3211.

Assertion

Ref	Expression
df-er	⊢ (Er R ↔ (◡R ∪ (R ∘ R)) ⊆ R)

Detailed syntax breakdown of Definition df-er

Step	Hyp	Ref	Expression
1		cR	. . 3 class R
2	1	wer 3197	. 2 wff Er R
3	1	ccnv 2409	. . . 4 class ◡R
4	1, 1	ccom 2414	. . . 4 class (R ∘ R)
5	3, 4	cun 1485	. . 3 class (◡R ∪ (R ∘ R))
6	5, 1	wss 1487	. 2 wff (◡R ∪ (R ∘ R)) ⊆ R
7	2, 6	wb 127	1 wff (Er R ↔ (◡R ∪ (R ∘ R)) ⊆ R)

This definition is referenced by:  er2 3201  ereq 3206

metamath.org