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 8281
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 8280). 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 8282. (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 8277 . 2 class [𝐴]𝑅
41csn 4559 . . 3 class {𝐴}
52, 4cima 5552 . 2 class (𝑅 “ {𝐴})
63, 5wceq 1528 1 wff [𝐴]𝑅 = (𝑅 “ {𝐴})
Colors of variables: wff setvar class
This definition is referenced by:  dfec2  8282  ecexg  8283  ecexr  8284  eceq1  8317  eceq2  8319  elecg  8322  ecss  8325  ecidsn  8332  uniqs  8347  ecqs  8351  ecinxp  8362  elecALTV  35410  uniqsALTV  35469  ecexALTV  35471  ec0  35503  prjspeclsp  39142
  Copyright terms: Public domain W3C validator