New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE 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. 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 5948. (Contributed by set.mm contributors, 22-Feb-2015.) |
Ref | Expression |
---|---|
df-ec |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cA | . . 3 | |
2 | cR | . . 3 | |
3 | 1, 2 | cec 5945 | . 2 |
4 | 1 | csn 3737 | . . 3 |
5 | 2, 4 | cima 4722 | . 2 |
6 | 3, 5 | wceq 1642 | 1 |
Colors of variables: wff setvar class |
This definition is referenced by: dfec2 5948 ecexg 5949 ecexr 5950 eceq1 5962 eceq2 5963 elec 5964 ecss 5966 ecidsn 5973 uniqs 5984 ecqs 5988 ecid 5989 |
Copyright terms: Public domain | W3C validator |