![]() |
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 8700). 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 8702. (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 8697 | . 2 class [𝐴]𝑅 |
4 | 1 | csn 4627 | . . 3 class {𝐴} |
5 | 2, 4 | cima 5678 | . 2 class (𝑅 “ {𝐴}) |
6 | 3, 5 | wceq 1541 | 1 wff [𝐴]𝑅 = (𝑅 “ {𝐴}) |
Colors of variables: wff setvar class |
This definition is referenced by: dfec2 8702 ecexg 8703 ecexr 8704 eceq1 8737 eceq2 8739 elecg 8742 ecss 8745 ecidsn 8752 uniqs 8767 ecqs 8771 ecinxp 8782 eqg0subgecsn 19068 lsmsnorb 32489 elecALTV 37122 uniqsALTV 37186 ecexALTV 37188 ec0 37226 prjspeclsp 41350 |
Copyright terms: Public domain | W3C validator |