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

Definition df-qs 7793
Description: Define quotient set. 𝑅 is usually an equivalence relation. Definition of [Enderton] p. 58. (Contributed by NM, 23-Jul-1995.)
Assertion
Ref Expression
df-qs (𝐴 / 𝑅) = {𝑦 ∣ ∃𝑥𝐴 𝑦 = [𝑥]𝑅}
Distinct variable groups:   𝑥,𝑦,𝐴   𝑥,𝑅,𝑦

Detailed syntax breakdown of Definition df-qs
StepHypRef Expression
1 cA . . 3 class 𝐴
2 cR . . 3 class 𝑅
31, 2cqs 7786 . 2 class (𝐴 / 𝑅)
4 vy . . . . . 6 setvar 𝑦
54cv 1522 . . . . 5 class 𝑦
6 vx . . . . . . 7 setvar 𝑥
76cv 1522 . . . . . 6 class 𝑥
87, 2cec 7785 . . . . 5 class [𝑥]𝑅
95, 8wceq 1523 . . . 4 wff 𝑦 = [𝑥]𝑅
109, 6, 1wrex 2942 . . 3 wff 𝑥𝐴 𝑦 = [𝑥]𝑅
1110, 4cab 2637 . 2 class {𝑦 ∣ ∃𝑥𝐴 𝑦 = [𝑥]𝑅}
123, 11wceq 1523 1 wff (𝐴 / 𝑅) = {𝑦 ∣ ∃𝑥𝐴 𝑦 = [𝑥]𝑅}
Colors of variables: wff setvar class
This definition is referenced by:  qseq1  7839  qseq2  7840  elqsg  7841  qsexg  7848  uniqs  7850  snec  7853  qsinxp  7866  qliftf  7878  quslem  16250  pi1xfrf  22899  pi1cof  22905  qsss1  34194  qsresid  34237  uniqsALTV  34242  0qs  34272
  Copyright terms: Public domain W3C validator