Definition df-ec 8684

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 8683). 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 8685. (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 8680	. 2 class [𝐴]𝑅
4	1	csn 4585	. . 3 class {𝐴}
5	2, 4	cima 5654	. 2 class (𝑅 “ {𝐴})
6	3, 5	wceq 1563	1 wff [𝐴]𝑅 = (𝑅 “ {𝐴})

This definition is referenced by:  dfec2  8685  ecexg  8686  ecexr  8687  eceq1  8722  eceq2  8724  elecg  8727  ecss  8734  ecidsn  8741  uniqs  8759  ecqs  8765  ecinxp  8778  eqg0subgecsn  19256  lsmsnorb  33615  elecALTV  38777  ec0  38883  dfqmap2  38953  prjspeclsp  43201