Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > df-ec | Structured version Visualization version GIF version |
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 8280). 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 8282. (Contributed by NM, 23-Jul-1995.) |
Ref | Expression |
---|---|
df-ec | ⊢ [𝐴]𝑅 = (𝑅 “ {𝐴}) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cA | . . 3 class 𝐴 | |
2 | cR | . . 3 class 𝑅 | |
3 | 1, 2 | cec 8277 | . 2 class [𝐴]𝑅 |
4 | 1 | csn 4559 | . . 3 class {𝐴} |
5 | 2, 4 | cima 5552 | . 2 class (𝑅 “ {𝐴}) |
6 | 3, 5 | wceq 1528 | 1 wff [𝐴]𝑅 = (𝑅 “ {𝐴}) |
Colors of variables: wff setvar class |
This definition is referenced by: dfec2 8282 ecexg 8283 ecexr 8284 eceq1 8317 eceq2 8319 elecg 8322 ecss 8325 ecidsn 8332 uniqs 8347 ecqs 8351 ecinxp 8362 elecALTV 35410 uniqsALTV 35469 ecexALTV 35471 ec0 35503 prjspeclsp 39142 |
Copyright terms: Public domain | W3C validator |