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 Er ; see dfer2 7331). 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 [ A ] (subscript) , although
we simply follow the brackets by since we don't have subscripted
expressions. For an alternate definition, see dfec2 7333. (Contributed by
NM, 23Jul1995.) 
Ref  Expression 

dfec 
Step  Hyp  Ref  Expression 

1  cA  . . 3  
2  cR  . . 3  
3  1, 2  cec 7328  . 2 
4  1  csn 4029  . . 3 
5  2, 4  cima 5007  . 2 
6  3, 5  wceq 1395  1 
Colors of variables: wff setvar class 
This definition is referenced by: dfec2 7333 ecexg 7334 ecexr 7335 eceq1 7366 eceq2 7368 elecg 7369 ecss 7372 ecidsn 7379 uniqs 7390 ecqs 7394 ecinxp 7405 
Copyright terms: Public domain  W3C validator 