Definition df-ec 8673

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 8672). 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 8674. (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 8669	. 2 class [𝐴]𝑅
4	1	csn 4579	. . 3 class {𝐴}
5	2, 4	cima 5646	. 2 class (𝑅 “ {𝐴})
6	3, 5	wceq 1559	1 wff [𝐴]𝑅 = (𝑅 “ {𝐴})

This definition is referenced by:  dfec2  8674  ecexg  8675  ecexr  8676  eceq1  8711  eceq2  8713  elecg  8716  ecss  8723  ecidsn  8730  uniqs  8748  ecqs  8754  ecinxp  8767  eqg0subgecsn  19228  lsmsnorb  33537  elecALTV  38730  ec0  38836  dfqmap2  38906  prjspeclsp  43154