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 6307). 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 6309. (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 6304 | . 2 class [𝐴]𝑅 |
4 | 1 | csn 3450 | . . 3 class {𝐴} |
5 | 2, 4 | cima 4455 | . 2 class (𝑅 “ {𝐴}) |
6 | 3, 5 | wceq 1290 | 1 wff [𝐴]𝑅 = (𝑅 “ {𝐴}) |
Colors of variables: wff set class |
This definition is referenced by: dfec2 6309 ecexg 6310 ecexr 6311 eceq1 6341 eceq2 6343 elecg 6344 ecss 6347 ecidsn 6353 uniqs 6364 ecqs 6368 ecinxp 6381 |
Copyright terms: Public domain | W3C validator |