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 7902
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 7895 . 2 class (𝐴 / 𝑅)
4 vy . . . . . 6 setvar 𝑦
54cv 1630 . . . . 5 class 𝑦
6 vx . . . . . . 7 setvar 𝑥
76cv 1630 . . . . . 6 class 𝑥
87, 2cec 7894 . . . . 5 class [𝑥]𝑅
95, 8wceq 1631 . . . 4 wff 𝑦 = [𝑥]𝑅
109, 6, 1wrex 3062 . . 3 wff 𝑥𝐴 𝑦 = [𝑥]𝑅
1110, 4cab 2757 . 2 class {𝑦 ∣ ∃𝑥𝐴 𝑦 = [𝑥]𝑅}
123, 11wceq 1631 1 wff (𝐴 / 𝑅) = {𝑦 ∣ ∃𝑥𝐴 𝑦 = [𝑥]𝑅}
Colors of variables: wff setvar class
This definition is referenced by:  qseq1  7948  qseq2  7949  elqsg  7950  qsexg  7957  uniqs  7959  snec  7962  qsinxp  7975  qliftf  7987  quslem  16411  pi1xfrf  23072  pi1cof  23078  qsss1  34396  qsresid  34439  uniqsALTV  34444  0qs  34474
  Copyright terms: Public domain W3C validator