Definition df-ec 8458

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 8457). 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 8459. (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 8454	. 2 class [𝐴]𝑅
4	1	csn 4558	. . 3 class {𝐴}
5	2, 4	cima 5583	. 2 class (𝑅 “ {𝐴})
6	3, 5	wceq 1539	1 wff [𝐴]𝑅 = (𝑅 “ {𝐴})

This definition is referenced by:  dfec2  8459  ecexg  8460  ecexr  8461  eceq1  8494  eceq2  8496  elecg  8499  ecss  8502  ecidsn  8509  uniqs  8524  ecqs  8528  ecinxp  8539  lsmsnorb  31481  elecALTV  36332  uniqsALTV  36391  ecexALTV  36393  ec0  36426  prjspeclsp  40372