Definition df-ec 8703

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 8702). 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 8704. (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 8699	. 2 class [𝐴]𝑅
4	1	csn 4584	. . 3 class {𝐴}
5	2, 4	cima 5654	. 2 class (𝑅 “ {𝐴})
6	3, 5	wceq 1570	1 wff [𝐴]𝑅 = (𝑅 “ {𝐴})

This definition is used by:  dfec2  8704  ecexg  8705  ecexr  8706  eceq1  8741  eceq2  8743  elecg  8746  ecss  8753  ecidsn  8760  uniqs  8778  ecqs  8784  ecinxp  8797  eqg0subgecsn  19392  lsmsnorb  33928  elecALTV  39171  ec0  39277  dfqmap2  39347  prjspeclsp  43602