Definition df-ec 8146

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 8145). 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 8147. (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 8142	. 2 class [𝐴]𝑅
4	1	csn 4476	. . 3 class {𝐴}
5	2, 4	cima 5451	. 2 class (𝑅 “ {𝐴})
6	3, 5	wceq 1522	1 wff [𝐴]𝑅 = (𝑅 “ {𝐴})

This definition is referenced by:  dfec2  8147  ecexg  8148  ecexr  8149  eceq1  8182  eceq2  8184  elecg  8187  ecss  8190  ecidsn  8197  uniqs  8212  ecqs  8216  ecinxp  8227  elecALTV  35084  uniqsALTV  35143  ecexALTV  35145  ec0  35177  prjspeclsp  38784