Definition df-ec 8723

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 8722). 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 8724. (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 8719	. 2 class [𝐴]𝑅
4	1	csn 4584	. . 3 class {𝐴}
5	2, 4	cima 5653	. 2 class (𝑅 “ {𝐴})
6	3, 5	wceq 1569	1 wff [𝐴]𝑅 = (𝑅 “ {𝐴})

This definition is used by:  dfec2  8724  ecexg  8725  ecexr  8726  eceq1  8761  eceq2  8763  elecg  8766  ecss  8773  ecidsn  8780  uniqs  8798  ecqs  8804  ecinxp  8817  eqg0subgecsn  19418  lsmsnorb  33993  elecALTV  39297  ec0  39403  dfqmap2  39473  prjspeclsp  43734