Definition df-ec 8705

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

This definition is used by:  dfec2  8706  ecexg  8707  ecexr  8708  eceq1  8743  eceq2  8745  elecg  8748  ecss  8755  ecidsn  8762  uniqs  8780  ecqs  8786  ecinxp  8799  eqg0subgecsn  19299  lsmsnorb  33735  elecALTV  38961  ec0  39067  dfqmap2  39137  prjspeclsp  43385