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 8747
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 8746). 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 8748. (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 8743 . 2 class [𝐴]𝑅
41csn 4626 . . 3 class {𝐴}
52, 4cima 5688 . 2 class (𝑅 “ {𝐴})
63, 5wceq 1540 1 wff [𝐴]𝑅 = (𝑅 “ {𝐴})
Colors of variables: wff setvar class
This definition is referenced by:  dfec2  8748  ecexg  8749  ecexr  8750  eceq1  8784  eceq2  8786  elecg  8789  ecss  8793  ecidsn  8800  uniqs  8817  ecqs  8821  ecinxp  8832  eqg0subgecsn  19215  lsmsnorb  33419  elecALTV  38267  uniqsALTV  38330  ecexALTV  38332  ec0  38370  prjspeclsp  42622
  Copyright terms: Public domain W3C validator