Definition df-er 7629

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 7630 we derive a more typical definition. We show that an equivalence relation is reflexive, symmetric, and transitive in erref 7649, ersymb 7643, and ertr 7644. (Contributed by NM, 4-Jun-1995.) (Revised by Mario Carneiro, 2-Nov-2015.)

Assertion

Ref	Expression
df-er	⊢ (𝑅 Er 𝐴 ↔ (Rel 𝑅 ∧ dom 𝑅 = 𝐴 ∧ (◡𝑅 ∪ (𝑅 ∘ 𝑅)) ⊆ 𝑅))

Detailed syntax breakdown of Definition df-er

Step	Hyp	Ref	Expression
1		cA	. . 3 class 𝐴
2		cR	. . 3 class 𝑅
3	1, 2	wer 7626	. 2 wff 𝑅 Er 𝐴
4	2	wrel 5043	. . 3 wff Rel 𝑅
5	2	cdm 5038	. . . 4 class dom 𝑅
6	5, 1	wceq 1475	. . 3 wff dom 𝑅 = 𝐴
7	2	ccnv 5037	. . . . 5 class ◡𝑅
8	2, 2	ccom 5042	. . . . 5 class (𝑅 ∘ 𝑅)
9	7, 8	cun 3538	. . . 4 class (◡𝑅 ∪ (𝑅 ∘ 𝑅))
10	9, 2	wss 3540	. . 3 wff (◡𝑅 ∪ (𝑅 ∘ 𝑅)) ⊆ 𝑅
11	4, 6, 10	w3a 1031	. 2 wff (Rel 𝑅 ∧ dom 𝑅 = 𝐴 ∧ (◡𝑅 ∪ (𝑅 ∘ 𝑅)) ⊆ 𝑅)
12	3, 11	wb 195	1 wff (𝑅 Er 𝐴 ↔ (Rel 𝑅 ∧ dom 𝑅 = 𝐴 ∧ (◡𝑅 ∪ (𝑅 ∘ 𝑅)) ⊆ 𝑅))

This definition is referenced by:  dfer2  7630  ereq1  7636  ereq2  7637  errel  7638  erdm  7639  ersym  7641  ertr  7644  xpider  7705  fcoinver  28798