Definition df-ec 8702

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 8701). 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 8703. (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 8698	. 2 class [𝐴]𝑅
4	1	csn 4587	. . 3 class {𝐴}
5	2, 4	cima 5662	. 2 class (𝑅 “ {𝐴})
6	3, 5	wceq 1570	1 wff [𝐴]𝑅 = (𝑅 “ {𝐴})

This definition is used by:  dfec2  8703  ecexg  8704  ecexr  8705  eceq1  8740  eceq2  8742  elecg  8745  ecss  8752  ecidsn  8759  uniqs  8777  ecqs  8783  ecinxp  8796  eqg0subgecsn  19331  lsmsnorb  33832  elecALTV  39027  ec0  39133  dfqmap2  39203  prjspeclsp  43466