Definition df-ec 8293

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 8292). 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 8294. (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 8289	. 2 class [𝐴]𝑅
4	1	csn 4569	. . 3 class {𝐴}
5	2, 4	cima 5560	. 2 class (𝑅 “ {𝐴})
6	3, 5	wceq 1537	1 wff [𝐴]𝑅 = (𝑅 “ {𝐴})

This definition is referenced by:  dfec2  8294  ecexg  8295  ecexr  8296  eceq1  8329  eceq2  8331  elecg  8334  ecss  8337  ecidsn  8344  uniqs  8359  ecqs  8363  ecinxp  8374  lsmsnorb  30947  elecALTV  35529  uniqsALTV  35588  ecexALTV  35590  ec0  35623  prjspeclsp  39269