Definition df-ec 8701

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 8700). 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 8702. (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 8697	. 2 class [𝐴]𝑅
4	1	csn 4627	. . 3 class {𝐴}
5	2, 4	cima 5678	. 2 class (𝑅 “ {𝐴})
6	3, 5	wceq 1542	1 wff [𝐴]𝑅 = (𝑅 “ {𝐴})

This definition is referenced by:  dfec2  8702  ecexg  8703  ecexr  8704  eceq1  8737  eceq2  8739  elecg  8742  ecss  8745  ecidsn  8752  uniqs  8767  ecqs  8771  ecinxp  8782  eqg0subgecsn  19068  lsmsnorb  32466  elecALTV  37072  uniqsALTV  37136  ecexALTV  37138  ec0  37176  prjspeclsp  41298