Definition df-ec 8692

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 8691). 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 8693. (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 8688	. 2 class [𝐴]𝑅
4	1	csn 4589	. . 3 class {𝐴}
5	2, 4	cima 5664	. 2 class (𝑅 “ {𝐴})
6	3, 5	wceq 1570	1 wff [𝐴]𝑅 = (𝑅 “ {𝐴})

This definition is used by:  dfec2  8693  ecexg  8694  ecexr  8695  eceq1  8730  eceq2  8732  elecg  8735  ecss  8742  ecidsn  8749  uniqs  8767  ecqs  8773  ecinxp  8786  eqg0subgecsn  19272  lsmsnorb  33713  elecALTV  38948  ec0  39054  dfqmap2  39124  prjspeclsp  43372