Definition df-ec 8500

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 8499). 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 8501. (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 8496	. 2 class [𝐴]𝑅
4	1	csn 4561	. . 3 class {𝐴}
5	2, 4	cima 5592	. 2 class (𝑅 “ {𝐴})
6	3, 5	wceq 1539	1 wff [𝐴]𝑅 = (𝑅 “ {𝐴})

This definition is referenced by:  dfec2  8501  ecexg  8502  ecexr  8503  eceq1  8536  eceq2  8538  elecg  8541  ecss  8544  ecidsn  8551  uniqs  8566  ecqs  8570  ecinxp  8581  lsmsnorb  31579  elecALTV  36405  uniqsALTV  36464  ecexALTV  36466  ec0  36499  prjspeclsp  40451