Definition df-er 6745

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 6746 we derive a more typical definition. We show that an equivalence relation is reflexive, symmetric, and transitive in erref 6765, ersymb 6759, and ertr 6760. (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

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2		cR	. . 3 class R
3	1, 2	wer 6742	. 2 wff R Er A
4	2	wrel 4736	. . 3 wff Rel R
5	2	cdm 4731	. . . 4 class dom R
6	5, 1	wceq 1398	. . 3 wff dom R = A
7	2	ccnv 4730	. . . . 5 class `' R
8	2, 2	ccom 4735	. . . . 5 class ( R o. R )
9	7, 8	cun 3199	. . . 4 class ( `' R u. ( R o. R ) )
10	9, 2	wss 3201	. . 3 wff ( `' R u. ( R o. R ) ) C_ R
11	4, 6, 10	w3a 1005	. 2 wff ( Rel R /\ dom R = A /\ ( `' R u. ( R o. R ) ) C_ R )
12	3, 11	wb 105	1 wff ( R Er A <-> ( Rel R /\ dom R = A /\ ( `' R u. ( R o. R ) ) C_ R ) )

This definition is referenced by:  dfer2  6746  ereq1  6752  ereq2  6753  errel  6754  erdm  6755  ersym  6757  ertr  6760  xpider  6818