Definition df-ec 8647

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 8646). 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 8648. (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 8643	. 2 class [𝐴]𝑅
4	1	csn 4582	. . 3 class {𝐴}
5	2, 4	cima 5635	. 2 class (𝑅 “ {𝐴})
6	3, 5	wceq 1542	1 wff [𝐴]𝑅 = (𝑅 “ {𝐴})

This definition is referenced by:  dfec2  8648  ecexg  8649  ecexr  8650  eceq1  8685  eceq2  8687  elecg  8690  ecss  8697  ecidsn  8704  uniqs  8722  ecqs  8728  ecinxp  8741  eqg0subgecsn  19138  lsmsnorb  33483  elecALTV  38519  ec0  38625  dfqmap2  38695  prjspeclsp  42967