Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > df-ec | 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 6498). 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 6500. (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 6495 | . 2 class [𝐴]𝑅 |
4 | 1 | csn 3575 | . . 3 class {𝐴} |
5 | 2, 4 | cima 4606 | . 2 class (𝑅 “ {𝐴}) |
6 | 3, 5 | wceq 1343 | 1 wff [𝐴]𝑅 = (𝑅 “ {𝐴}) |
Colors of variables: wff set class |
This definition is referenced by: dfec2 6500 ecexg 6501 ecexr 6502 eceq1 6532 eceq2 6534 elecg 6535 ecss 6538 ecidsn 6544 uniqs 6555 ecqs 6559 ecinxp 6572 |
Copyright terms: Public domain | W3C validator |