Definition df-ec 8630

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 8629). 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 8631. (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 8626	. 2 class [𝐴]𝑅
4	1	csn 4575	. . 3 class {𝐴}
5	2, 4	cima 5622	. 2 class (𝑅 “ {𝐴})
6	3, 5	wceq 1541	1 wff [𝐴]𝑅 = (𝑅 “ {𝐴})

This definition is referenced by:  dfec2  8631  ecexg  8632  ecexr  8633  eceq1  8667  eceq2  8669  elecg  8672  ecss  8679  ecidsn  8686  uniqs  8704  ecqs  8709  ecinxp  8722  eqg0subgecsn  19111  lsmsnorb  33363  elecALTV  38324  ec0  38422  prjspeclsp  42731