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 8751
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 8744 . 2 class (𝐴 / 𝑅)
4 vy . . . . . 6 setvar 𝑦
54cv 1539 . . . . 5 class 𝑦
6 vx . . . . . . 7 setvar 𝑥
76cv 1539 . . . . . 6 class 𝑥
87, 2cec 8743 . . . . 5 class [𝑥]𝑅
95, 8wceq 1540 . . . 4 wff 𝑦 = [𝑥]𝑅
109, 6, 1wrex 3070 . . 3 wff 𝑥𝐴 𝑦 = [𝑥]𝑅
1110, 4cab 2714 . 2 class {𝑦 ∣ ∃𝑥𝐴 𝑦 = [𝑥]𝑅}
123, 11wceq 1540 1 wff (𝐴 / 𝑅) = {𝑦 ∣ ∃𝑥𝐴 𝑦 = [𝑥]𝑅}
Colors of variables: wff setvar class
This definition is referenced by:  qseq1  8801  qseq2  8802  0qs  8807  elqsg  8808  qsexg  8815  uniqs  8817  snec  8820  qsinxp  8833  qliftf  8845  quslem  17588  qus0subgbas  19216  pzriprnglem11  21502  pi1xfrf  25086  pi1cof  25092  qusbas2  33434  qsss1  38290  qsresid  38326  uniqsALTV  38330  disjdmqscossss  38804  dfqs2  42278  dfqs3  42279
  Copyright terms: Public domain W3C validator