MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-ec Structured version   Visualization version   GIF version

Definition df-ec 8705
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 8704). 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 8706. (Contributed by NM, 23-Jul-1995.)
Assertion
Ref Expression
df-ec [𝐴]𝑅 = (𝑅 “ {𝐴})

Detailed syntax breakdown of Definition df-ec
StepHypRef Expression
1 cA . . 3 class 𝐴
2 cR . . 3 class 𝑅
31, 2cec 8701 . 2 class [𝐴]𝑅
41csn 4629 . . 3 class {𝐴}
52, 4cima 5680 . 2 class (𝑅 “ {𝐴})
63, 5wceq 1542 1 wff [𝐴]𝑅 = (𝑅 “ {𝐴})
Colors of variables: wff setvar class
This definition is referenced by:  dfec2  8706  ecexg  8707  ecexr  8708  eceq1  8741  eceq2  8743  elecg  8746  ecss  8749  ecidsn  8756  uniqs  8771  ecqs  8775  ecinxp  8786  eqg0subgecsn  19074  lsmsnorb  32501  elecALTV  37134  uniqsALTV  37198  ecexALTV  37200  ec0  37238  prjspeclsp  41354
  Copyright terms: Public domain W3C validator