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 8282
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 8275 . 2 class (𝐴 / 𝑅)
4 vy . . . . . 6 setvar 𝑦
54cv 1537 . . . . 5 class 𝑦
6 vx . . . . . . 7 setvar 𝑥
76cv 1537 . . . . . 6 class 𝑥
87, 2cec 8274 . . . . 5 class [𝑥]𝑅
95, 8wceq 1538 . . . 4 wff 𝑦 = [𝑥]𝑅
109, 6, 1wrex 3110 . . 3 wff 𝑥𝐴 𝑦 = [𝑥]𝑅
1110, 4cab 2779 . 2 class {𝑦 ∣ ∃𝑥𝐴 𝑦 = [𝑥]𝑅}
123, 11wceq 1538 1 wff (𝐴 / 𝑅) = {𝑦 ∣ ∃𝑥𝐴 𝑦 = [𝑥]𝑅}
Colors of variables: wff setvar class
This definition is referenced by:  qseq1  8330  qseq2  8331  elqsg  8335  qsexg  8342  uniqs  8344  snec  8347  qsinxp  8360  qliftf  8372  quslem  16812  pi1xfrf  23662  pi1cof  23668  qsss1  35704  qsresid  35741  uniqsALTV  35745  0qs  35781  dfqs2  39410  dfqs3  39411
  Copyright terms: Public domain W3C validator