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	⊢ ( 𝑅 Er 𝐴 ↔ ( Rel 𝑅 ∧ dom 𝑅 = 𝐴 ∧ ( ◡ 𝑅 ∪ ( 𝑅 ∘ 𝑅 ) ) ⊆ 𝑅 ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cR	⊢ 𝑅
1		cA	⊢ 𝐴
2	1 0	wer	⊢ 𝑅 Er 𝐴
3	0	wrel	⊢ Rel 𝑅
4	0	cdm	⊢ dom 𝑅
5	4 1	wceq	⊢ dom 𝑅 = 𝐴
6	0	ccnv	⊢ ◡ 𝑅
7	0 0	ccom	⊢ ( 𝑅 ∘ 𝑅 )
8	6 7	cun	⊢ ( ◡ 𝑅 ∪ ( 𝑅 ∘ 𝑅 ) )
9	8 0	wss	⊢ ( ◡ 𝑅 ∪ ( 𝑅 ∘ 𝑅 ) ) ⊆ 𝑅
10	3 5 9	w3a	⊢ ( Rel 𝑅 ∧ dom 𝑅 = 𝐴 ∧ ( ◡ 𝑅 ∪ ( 𝑅 ∘ 𝑅 ) ) ⊆ 𝑅 )
11	2 10	wb	⊢ ( 𝑅 Er 𝐴 ↔ ( Rel 𝑅 ∧ dom 𝑅 = 𝐴 ∧ ( ◡ 𝑅 ∪ ( 𝑅 ∘ 𝑅 ) ) ⊆ 𝑅 ) )