Definition df-ec 8645

Description: Define the 𝑅-coset of 𝐴. Exercise 35 of [Enderton] p. 61. This is called the equivalence class of 𝐴 modulo 𝑅 when 𝑅 is an equivalence relation (i.e. when Er 𝑅; see dfer2 8644). In this case, 𝐴 is a representative (member) of the equivalence class [𝐴]𝑅, which contains all sets that are equivalent to 𝐴. Definition of [Enderton] p. 57 uses the notation [𝐴] (subscript) 𝑅, although we simply follow the brackets by 𝑅 since we don't have subscripted expressions. For an alternate definition, see dfec2 8646. (Contributed by NM, 23-Jul-1995.)

Assertion

Ref	Expression
df-ec	⊢ [𝐴]𝑅 = (𝑅 “ {𝐴})

Detailed syntax breakdown of Definition df-ec

Step	Hyp	Ref	Expression
1		cA	. . 3 class 𝐴
2		cR	. . 3 class 𝑅
3	1, 2	cec 8641	. 2 class [𝐴]𝑅
4	1	csn 4567	. . 3 class {𝐴}
5	2, 4	cima 5634	. 2 class (𝑅 “ {𝐴})
6	3, 5	wceq 1542	1 wff [𝐴]𝑅 = (𝑅 “ {𝐴})

This definition is referenced by:  dfec2  8646  ecexg  8647  ecexr  8648  eceq1  8683  eceq2  8685  elecg  8688  ecss  8695  ecidsn  8702  uniqs  8720  ecqs  8726  ecinxp  8739  eqg0subgecsn  19172  lsmsnorb  33451  elecALTV  38592  ec0  38698  dfqmap2  38768  prjspeclsp  43045