Definition df-ec 8634

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 8633). 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 8635. (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 8630	. 2 class [𝐴]𝑅
4	1	csn 4579	. . 3 class {𝐴}
5	2, 4	cima 5626	. 2 class (𝑅 “ {𝐴})
6	3, 5	wceq 1540	1 wff [𝐴]𝑅 = (𝑅 “ {𝐴})

This definition is referenced by:  dfec2  8635  ecexg  8636  ecexr  8637  eceq1  8671  eceq2  8673  elecg  8676  ecss  8683  ecidsn  8690  uniqs  8708  ecqs  8713  ecinxp  8726  eqg0subgecsn  19094  lsmsnorb  33338  elecALTV  38240  ec0  38336  prjspeclsp  42585