Definition df-ec 8291

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 8290). 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 8292. (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 8287	. 2 class [𝐴]𝑅
4	1	csn 4567	. . 3 class {𝐴}
5	2, 4	cima 5558	. 2 class (𝑅 “ {𝐴})
6	3, 5	wceq 1537	1 wff [𝐴]𝑅 = (𝑅 “ {𝐴})

This definition is referenced by:  dfec2  8292  ecexg  8293  ecexr  8294  eceq1  8327  eceq2  8329  elecg  8332  ecss  8335  ecidsn  8342  uniqs  8357  ecqs  8361  ecinxp  8372  lsmsnorb  30945  elecALTV  35542  uniqsALTV  35601  ecexALTV  35603  ec0  35636  prjspeclsp  39311