| 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 8746). 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 8748. (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 8743 | . 2 class [𝐴]𝑅 |
| 4 | 1 | csn 4626 | . . 3 class {𝐴} |
| 5 | 2, 4 | cima 5688 | . 2 class (𝑅 “ {𝐴}) |
| 6 | 3, 5 | wceq 1540 | 1 wff [𝐴]𝑅 = (𝑅 “ {𝐴}) |
| Colors of variables: wff setvar class |
| This definition is referenced by: dfec2 8748 ecexg 8749 ecexr 8750 eceq1 8784 eceq2 8786 elecg 8789 ecss 8793 ecidsn 8800 uniqs 8817 ecqs 8821 ecinxp 8832 eqg0subgecsn 19215 lsmsnorb 33419 elecALTV 38267 uniqsALTV 38330 ecexALTV 38332 ec0 38370 prjspeclsp 42622 |
| Copyright terms: Public domain | W3C validator |