Definition df-ec 8709

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 8708). 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 8710. (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 8705	. 2 class [𝐴]𝑅
4	1	csn 4629	. . 3 class {𝐴}
5	2, 4	cima 5680	. 2 class (𝑅 “ {𝐴})
6	3, 5	wceq 1539	1 wff [𝐴]𝑅 = (𝑅 “ {𝐴})

This definition is referenced by:  dfec2  8710  ecexg  8711  ecexr  8712  eceq1  8745  eceq2  8747  elecg  8750  ecss  8753  ecidsn  8760  uniqs  8775  ecqs  8779  ecinxp  8790  eqg0subgecsn  19114  lsmsnorb  32773  elecALTV  37439  uniqsALTV  37503  ecexALTV  37505  ec0  37543  prjspeclsp  41658