![]() |
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 8744). 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 8746. (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 8741 | . 2 class [𝐴]𝑅 |
4 | 1 | csn 4630 | . . 3 class {𝐴} |
5 | 2, 4 | cima 5691 | . 2 class (𝑅 “ {𝐴}) |
6 | 3, 5 | wceq 1536 | 1 wff [𝐴]𝑅 = (𝑅 “ {𝐴}) |
Colors of variables: wff setvar class |
This definition is referenced by: dfec2 8746 ecexg 8747 ecexr 8748 eceq1 8782 eceq2 8784 elecg 8787 ecss 8791 ecidsn 8798 uniqs 8815 ecqs 8819 ecinxp 8830 eqg0subgecsn 19227 lsmsnorb 33398 elecALTV 38247 uniqsALTV 38310 ecexALTV 38312 ec0 38350 prjspeclsp 42598 |
Copyright terms: Public domain | W3C validator |