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 8285
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 8278 . 2 class (𝐴 / 𝑅)
4 vy . . . . . 6 setvar 𝑦
54cv 1527 . . . . 5 class 𝑦
6 vx . . . . . . 7 setvar 𝑥
76cv 1527 . . . . . 6 class 𝑥
87, 2cec 8277 . . . . 5 class [𝑥]𝑅
95, 8wceq 1528 . . . 4 wff 𝑦 = [𝑥]𝑅
109, 6, 1wrex 3139 . . 3 wff 𝑥𝐴 𝑦 = [𝑥]𝑅
1110, 4cab 2799 . 2 class {𝑦 ∣ ∃𝑥𝐴 𝑦 = [𝑥]𝑅}
123, 11wceq 1528 1 wff (𝐴 / 𝑅) = {𝑦 ∣ ∃𝑥𝐴 𝑦 = [𝑥]𝑅}
Colors of variables: wff setvar class
This definition is referenced by:  qseq1  8333  qseq2  8334  elqsg  8338  qsexg  8345  uniqs  8347  snec  8350  qsinxp  8363  qliftf  8375  quslem  16806  pi1xfrf  23586  pi1cof  23592  qsss1  35428  qsresid  35465  uniqsALTV  35469  0qs  35504  dfqs2  39002  dfqs3  39003
  Copyright terms: Public domain W3C validator