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 8145
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 8138 . 2 class (𝐴 / 𝑅)
4 vy . . . . . 6 setvar 𝑦
54cv 1521 . . . . 5 class 𝑦
6 vx . . . . . . 7 setvar 𝑥
76cv 1521 . . . . . 6 class 𝑥
87, 2cec 8137 . . . . 5 class [𝑥]𝑅
95, 8wceq 1522 . . . 4 wff 𝑦 = [𝑥]𝑅
109, 6, 1wrex 3106 . . 3 wff 𝑥𝐴 𝑦 = [𝑥]𝑅
1110, 4cab 2775 . 2 class {𝑦 ∣ ∃𝑥𝐴 𝑦 = [𝑥]𝑅}
123, 11wceq 1522 1 wff (𝐴 / 𝑅) = {𝑦 ∣ ∃𝑥𝐴 𝑦 = [𝑥]𝑅}
Colors of variables: wff setvar class
This definition is referenced by:  qseq1  8193  qseq2  8194  elqsg  8198  qsexg  8205  uniqs  8207  snec  8210  qsinxp  8223  qliftf  8235  quslem  16645  pi1xfrf  23340  pi1cof  23346  qsss1  35077  qsresid  35114  uniqsALTV  35118  0qs  35153  dfqs2  38652  dfqs3  38653
  Copyright terms: Public domain W3C validator