Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > df-ec | Unicode 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 ; see dfer2 6423). 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 6425. (Contributed by NM, 23-Jul-1995.) |
Ref | Expression |
---|---|
df-ec |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cA | . . 3 | |
2 | cR | . . 3 | |
3 | 1, 2 | cec 6420 | . 2 |
4 | 1 | csn 3522 | . . 3 |
5 | 2, 4 | cima 4537 | . 2 |
6 | 3, 5 | wceq 1331 | 1 |
Colors of variables: wff set class |
This definition is referenced by: dfec2 6425 ecexg 6426 ecexr 6427 eceq1 6457 eceq2 6459 elecg 6460 ecss 6463 ecidsn 6469 uniqs 6480 ecqs 6484 ecinxp 6497 |
Copyright terms: Public domain | W3C validator |