Definition df-ec 8697

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

This definition is referenced by:  dfec2  8698  ecexg  8699  ecexr  8700  eceq1  8735  eceq2  8737  elecg  8740  ecss  8747  ecidsn  8754  uniqs  8772  ecqs  8778  ecinxp  8791  eqg0subgecsn  19269  lsmsnorb  33685  elecALTV  38901  ec0  39007  dfqmap2  39077  prjspeclsp  43327