Definition df-ec 8638

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 8637). 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 8639. (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 8634	. 2 class [𝐴]𝑅
4	1	csn 4568	. . 3 class {𝐴}
5	2, 4	cima 5627	. 2 class (𝑅 “ {𝐴})
6	3, 5	wceq 1542	1 wff [𝐴]𝑅 = (𝑅 “ {𝐴})

This definition is referenced by:  dfec2  8639  ecexg  8640  ecexr  8641  eceq1  8676  eceq2  8678  elecg  8681  ecss  8688  ecidsn  8695  uniqs  8713  ecqs  8719  ecinxp  8732  eqg0subgecsn  19163  lsmsnorb  33466  elecALTV  38606  ec0  38712  dfqmap2  38782  prjspeclsp  43059