![]() |
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 8704). 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 8706. (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 8701 | . 2 class [𝐴]𝑅 |
4 | 1 | csn 4629 | . . 3 class {𝐴} |
5 | 2, 4 | cima 5680 | . 2 class (𝑅 “ {𝐴}) |
6 | 3, 5 | wceq 1542 | 1 wff [𝐴]𝑅 = (𝑅 “ {𝐴}) |
Colors of variables: wff setvar class |
This definition is referenced by: dfec2 8706 ecexg 8707 ecexr 8708 eceq1 8741 eceq2 8743 elecg 8746 ecss 8749 ecidsn 8756 uniqs 8771 ecqs 8775 ecinxp 8786 eqg0subgecsn 19074 lsmsnorb 32501 elecALTV 37134 uniqsALTV 37198 ecexALTV 37200 ec0 37238 prjspeclsp 41354 |
Copyright terms: Public domain | W3C validator |