NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  df-ec Unicode version

Definition df-ec 5947
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.)
Assertion
Ref Expression
df-ec

Detailed syntax breakdown of Definition df-ec
StepHypRef Expression
1 cA . . 3
2 cR . . 3
31, 2cec 5945 . 2
41csn 3737 . . 3
52, 4cima 4722 . 2
63, 5wceq 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