Definition df-ec 8308

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 8307). 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 8309. (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 8304	. 2 class [𝐴]𝑅
4	1	csn 4526	. . 3 class {𝐴}
5	2, 4	cima 5532	. 2 class (𝑅 “ {𝐴})
6	3, 5	wceq 1539	1 wff [𝐴]𝑅 = (𝑅 “ {𝐴})

This definition is referenced by:  dfec2  8309  ecexg  8310  ecexr  8311  eceq1  8344  eceq2  8346  elecg  8349  ecss  8352  ecidsn  8359  uniqs  8374  ecqs  8378  ecinxp  8389  lsmsnorb  31114  elecALTV  36003  uniqsALTV  36062  ecexALTV  36064  ec0  36097  prjspeclsp  39994