Definition df-ec 8676

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 8675). 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 8677. (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 8672	. 2 class [𝐴]𝑅
4	1	csn 4592	. . 3 class {𝐴}
5	2, 4	cima 5644	. 2 class (𝑅 “ {𝐴})
6	3, 5	wceq 1540	1 wff [𝐴]𝑅 = (𝑅 “ {𝐴})

This definition is referenced by:  dfec2  8677  ecexg  8678  ecexr  8679  eceq1  8713  eceq2  8715  elecg  8718  ecss  8725  ecidsn  8732  uniqs  8750  ecqs  8755  ecinxp  8768  eqg0subgecsn  19136  lsmsnorb  33369  elecALTV  38262  ec0  38358  prjspeclsp  42607