Definition df-ec 8642

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 8641). 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 8643. (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 8638	. 2 class [𝐴]𝑅
4	1	csn 4562	. . 3 class {𝐴}
5	2, 4	cima 5628	. 2 class (𝑅 “ {𝐴})
6	3, 5	wceq 1547	1 wff [𝐴]𝑅 = (𝑅 “ {𝐴})

This definition is referenced by:  dfec2  8643  ecexg  8644  ecexr  8645  eceq1  8680  eceq2  8682  elecg  8685  ecss  8692  ecidsn  8699  uniqs  8717  ecqs  8723  ecinxp  8736  eqg0subgecsn  19170  lsmsnorb  33481  elecALTV  38645  ec0  38751  dfqmap2  38821  prjspeclsp  43069