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 8740
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 8733 . 2 class (𝐴 / 𝑅)
4 vy . . . . . 6 setvar 𝑦
54cv 1533 . . . . 5 class 𝑦
6 vx . . . . . . 7 setvar 𝑥
76cv 1533 . . . . . 6 class 𝑥
87, 2cec 8732 . . . . 5 class [𝑥]𝑅
95, 8wceq 1534 . . . 4 wff 𝑦 = [𝑥]𝑅
109, 6, 1wrex 3060 . . 3 wff 𝑥𝐴 𝑦 = [𝑥]𝑅
1110, 4cab 2703 . 2 class {𝑦 ∣ ∃𝑥𝐴 𝑦 = [𝑥]𝑅}
123, 11wceq 1534 1 wff (𝐴 / 𝑅) = {𝑦 ∣ ∃𝑥𝐴 𝑦 = [𝑥]𝑅}
Colors of variables: wff setvar class
This definition is referenced by:  qseq1  8790  qseq2  8791  0qs  8796  elqsg  8797  qsexg  8804  uniqs  8806  snec  8809  qsinxp  8822  qliftf  8834  quslem  17558  qus0subgbas  19192  pzriprnglem11  21481  pi1xfrf  25071  pi1cof  25077  qusbas2  33281  qsss1  37987  qsresid  38023  uniqsALTV  38027  disjdmqscossss  38501  dfqs2  41961  dfqs3  41962
  Copyright terms: Public domain W3C validator