Definition df-ec 8633

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

This definition is referenced by:  dfec2  8634  ecexg  8635  ecexr  8636  eceq1  8670  eceq2  8672  elecg  8675  ecss  8682  ecidsn  8689  uniqs  8707  ecqs  8712  ecinxp  8725  eqg0subgecsn  19119  lsmsnorb  33367  elecALTV  38313  ec0  38411  prjspeclsp  42720