Definition df-ec 8624

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 8623). 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 8625. (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 8620	. 2 class [𝐴]𝑅
4	1	csn 4576	. . 3 class {𝐴}
5	2, 4	cima 5619	. 2 class (𝑅 “ {𝐴})
6	3, 5	wceq 1541	1 wff [𝐴]𝑅 = (𝑅 “ {𝐴})

This definition is referenced by:  dfec2  8625  ecexg  8626  ecexr  8627  eceq1  8661  eceq2  8663  elecg  8666  ecss  8673  ecidsn  8680  uniqs  8698  ecqs  8703  ecinxp  8716  eqg0subgecsn  19107  lsmsnorb  33351  elecALTV  38300  ec0  38396  prjspeclsp  42644