This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Definition df-er

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)

		Ref	Expression
	Assertion	df-er	\|- ( R Er A <-> ( Rel R /\ dom R = A /\ ( `' R u. ( R o. R ) ) C_ R ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cR	\|- R
1		cA	\|- A
2	1 0	wer	\|- R Er A
3	0	wrel	\|- Rel R
4	0	cdm	\|- dom R
5	4 1	wceq	\|- dom R = A
6	0	ccnv	\|- `' R
7	0 0	ccom	\|- ( R o. R )
8	6 7	cun	\|- ( `' R u. ( R o. R ) )
9	8 0	wss	\|- ( `' R u. ( R o. R ) ) C_ R
10	3 5 9	w3a	\|- ( Rel R /\ dom R = A /\ ( `' R u. ( R o. R ) ) C_ R )
11	2 10	wb	\|- ( R Er A <-> ( Rel R /\ dom R = A /\ ( `' R u. ( R o. R ) ) C_ R ) )