Definition df-ec 8755

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 8754). 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 8756. (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 8751	. 2 class [𝐴]𝑅
4	1	csn 4588	. . 3 class {𝐴}
5	2, 4	cima 5659	. 2 class (𝑅 “ {𝐴})
6	3, 5	wceq 1570	1 wff [𝐴]𝑅 = (𝑅 “ {𝐴})

This definition is used by:  dfec2  8756  ecexg  8757  ecexr  8758  eceq1  8793  eceq2  8795  elecg  8798  ecss  8805  ecidsn  8812  uniqs  8830  ecqs  8836  ecinxp  8849  eqg0subgecsn  19453  lsmsnorb  34043  elecALTV  39462  ec0  39568  dfqmap2  39638  prjspeclsp  43900