Definition df-ec 8719

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 8718). 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 8720. (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 8715	. 2 class [𝐴]𝑅
4	1	csn 4601	. . 3 class {𝐴}
5	2, 4	cima 5657	. 2 class (𝑅 “ {𝐴})
6	3, 5	wceq 1540	1 wff [𝐴]𝑅 = (𝑅 “ {𝐴})

This definition is referenced by:  dfec2  8720  ecexg  8721  ecexr  8722  eceq1  8756  eceq2  8758  elecg  8761  ecss  8765  ecidsn  8772  uniqs  8789  ecqs  8793  ecinxp  8804  eqg0subgecsn  19178  lsmsnorb  33352  elecALTV  38230  uniqsALTV  38293  ecexALTV  38295  ec0  38333  prjspeclsp  42582