Metamath Proof Explorer 
< Previous
Next >
Nearby theorems 

Mirrors > Home > MPE Home > Th. List > dfec  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 6547). 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 6549. (Contributed by NM, 23Jul1995.) 
Ref  Expression 

dfec 
Step  Hyp  Ref  Expression 

1  cA  . . 3  
2  cR  . . 3  
3  1, 2  cec 6544  . 2 
4  1  csn 3544  . . 3 
5  2, 4  cima 4583  . 2 
6  3, 5  wceq 1619  1 
Colors of variables: wff set class 
This definition is referenced by: dfec2 6549 ecexg 6550 ecexr 6551 eceq1 6582 eceq2 6583 elecg 6584 ecss 6587 ecidsn 6594 uniqs 6605 ecqs 6609 ecinxp 6620 
Copyright terms: Public domain  W3C validator 