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

Definition df-ec 5947
 Description: Define the R-coset of A. Exercise 35 of [Enderton] p. 61. This is called the equivalence class of A modulo R when R is an equivalence relation. In this case, A is a representative (member) of the equivalence class [A]R, which contains all sets that are equivalent to A. Definition of [Enderton] p. 57 uses the notation [A] (subscript) R, although we simply follow the brackets by R 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 [A]R = (R “ {A})

Detailed syntax breakdown of Definition df-ec
StepHypRef Expression
1 cA . . 3 class A
2 cR . . 3 class R
31, 2cec 5945 . 2 class [A]R
41csn 3737 . . 3 class {A}
52, 4cima 4722 . 2 class (R “ {A})
63, 5wceq 1642 1 wff [A]R = (R “ {A})
 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