Definition df-ec 8765

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 8764). 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 8766. (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 8761	. 2 class [𝐴]𝑅
4	1	csn 4648	. . 3 class {𝐴}
5	2, 4	cima 5703	. 2 class (𝑅 “ {𝐴})
6	3, 5	wceq 1537	1 wff [𝐴]𝑅 = (𝑅 “ {𝐴})

This definition is referenced by:  dfec2  8766  ecexg  8767  ecexr  8768  eceq1  8802  eceq2  8804  elecg  8807  ecss  8811  ecidsn  8818  uniqs  8835  ecqs  8839  ecinxp  8850  eqg0subgecsn  19237  lsmsnorb  33384  elecALTV  38222  uniqsALTV  38285  ecexALTV  38287  ec0  38325  prjspeclsp  42567