![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > df-ec | GIF version |
Description: Define the 𝑅-coset of A. Exercise 35 of [Enderton] p. 61. This is called the equivalence class of A modulo 𝑅 when 𝑅 is an equivalence relation (i.e. when Er 𝑅; see dfer2 6043). In this case, A is a representative (member) of the equivalence class [A]𝑅, which contains all sets that are equivalent to A. Definition of [Enderton] p. 57 uses the notation [A] (subscript) 𝑅, although we simply follow the brackets by 𝑅 since we don't have subscripted expressions. For an alternate definition, see dfec2 6045. (Contributed by NM, 23-Jul-1995.) |
Ref | Expression |
---|---|
df-ec | ⊢ [A]𝑅 = (𝑅 “ {A}) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cA | . . 3 class A | |
2 | cR | . . 3 class 𝑅 | |
3 | 1, 2 | cec 6040 | . 2 class [A]𝑅 |
4 | 1 | csn 3367 | . . 3 class {A} |
5 | 2, 4 | cima 4291 | . 2 class (𝑅 “ {A}) |
6 | 3, 5 | wceq 1242 | 1 wff [A]𝑅 = (𝑅 “ {A}) |
Colors of variables: wff set class |
This definition is referenced by: dfec2 6045 ecexg 6046 ecexr 6047 eceq1 6077 eceq2 6079 elecg 6080 ecss 6083 ecidsn 6089 uniqs 6100 ecqs 6104 ecinxp 6117 |
Copyright terms: Public domain | W3C validator |