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 8745
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 8744). 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 8746. (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 8741 . 2 class [𝐴]𝑅
41csn 4630 . . 3 class {𝐴}
52, 4cima 5691 . 2 class (𝑅 “ {𝐴})
63, 5wceq 1536 1 wff [𝐴]𝑅 = (𝑅 “ {𝐴})
Colors of variables: wff setvar class
This definition is referenced by:  dfec2  8746  ecexg  8747  ecexr  8748  eceq1  8782  eceq2  8784  elecg  8787  ecss  8791  ecidsn  8798  uniqs  8815  ecqs  8819  ecinxp  8830  eqg0subgecsn  19227  lsmsnorb  33398  elecALTV  38247  uniqsALTV  38310  ecexALTV  38312  ec0  38350  prjspeclsp  42598
  Copyright terms: Public domain W3C validator