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 7981
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 7974 . 2 class (𝐴 / 𝑅)
4 vy . . . . . 6 setvar 𝑦
54cv 1636 . . . . 5 class 𝑦
6 vx . . . . . . 7 setvar 𝑥
76cv 1636 . . . . . 6 class 𝑥
87, 2cec 7973 . . . . 5 class [𝑥]𝑅
95, 8wceq 1637 . . . 4 wff 𝑦 = [𝑥]𝑅
109, 6, 1wrex 3097 . . 3 wff 𝑥𝐴 𝑦 = [𝑥]𝑅
1110, 4cab 2792 . 2 class {𝑦 ∣ ∃𝑥𝐴 𝑦 = [𝑥]𝑅}
123, 11wceq 1637 1 wff (𝐴 / 𝑅) = {𝑦 ∣ ∃𝑥𝐴 𝑦 = [𝑥]𝑅}
Colors of variables: wff setvar class
This definition is referenced by:  qseq1  8027  qseq2  8028  elqsg  8029  qsexg  8036  uniqs  8038  snec  8041  qsinxp  8054  qliftf  8066  quslem  16404  pi1xfrf  23062  pi1cof  23068  qsss1  34368  qsresid  34409  uniqsALTV  34414  0qs  34443
  Copyright terms: Public domain W3C validator