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 \leftrightarrow (Rel R \land dom R = A \land R^{-1} \cup (R \circ R) \subseteq R)$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cR	$class R$
1		cA	$class A$
2	1 0	wer	$wff R Er A$
3	0	wrel	$wff Rel R$
4	0	cdm	$class dom R$
5	4 1	wceq	$wff dom R = A$
6	0	ccnv	$class R^{-1}$
7	0 0	ccom	$class (R \circ R)$
8	6 7	cun	$class (R^{-1} \cup (R \circ R))$
9	8 0	wss	$wff R^{-1} \cup (R \circ R) \subseteq R$
10	3 5 9	w3a	$wff (Rel R \land dom R = A \land R^{-1} \cup (R \circ R) \subseteq R)$
11	2 10	wb	$wff (R Er A \leftrightarrow (Rel R \land dom R = A \land R^{-1} \cup (R \circ R) \subseteq R))$

Metamath Proof Explorer

Definition df-er

Detailed syntax breakdown