Definition df-ec 8637

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 8636). 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 8638. (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 8633	. 2 class [𝐴]𝑅
4	1	csn 4580	. . 3 class {𝐴}
5	2, 4	cima 5627	. 2 class (𝑅 “ {𝐴})
6	3, 5	wceq 1541	1 wff [𝐴]𝑅 = (𝑅 “ {𝐴})

This definition is referenced by:  dfec2  8638  ecexg  8639  ecexr  8640  eceq1  8674  eceq2  8676  elecg  8679  ecss  8686  ecidsn  8693  uniqs  8711  ecqs  8716  ecinxp  8729  eqg0subgecsn  19126  lsmsnorb  33472  elecALTV  38464  ec0  38562  prjspeclsp  42855