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

Detailed syntax breakdown

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