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 8678
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 8671 . 2 class (𝐴 / 𝑅)
4 vy . . . . . 6 setvar 𝑦
54cv 1558 . . . . 5 class 𝑦
6 vx . . . . . . 7 setvar 𝑥
76cv 1558 . . . . . 6 class 𝑥
87, 2cec 8670 . . . . 5 class [𝑥]𝑅
95, 8wceq 1559 . . . 4 wff 𝑦 = [𝑥]𝑅
109, 6, 1wrex 3085 . . 3 wff 𝑥𝐴 𝑦 = [𝑥]𝑅
1110, 4cab 2739 . 2 class {𝑦 ∣ ∃𝑥𝐴 𝑦 = [𝑥]𝑅}
123, 11wceq 1559 1 wff (𝐴 / 𝑅) = {𝑦 ∣ ∃𝑥𝐴 𝑦 = [𝑥]𝑅}
Colors of variables: wff setvar class
This definition is referenced by:  dfqs2  8679  qseq1  8732  qseq2  8733  0qs  8738  elqsg  8739  qsexg  8747  uniqs  8749  snecg  8753  snec  8754  qsinxp  8769  qliftf  8781  quslem  17564  qus0subgbas  19230  pzriprnglem11  21531  pi1xfrf  25103  pi1cof  25109  qusbas2  33553  qsss1  38755  qsresid  38791  raldmqsmo  38823  qseq  39193  disjdmqscossss  39366  dfqs3  42816
  Copyright terms: Public domain W3C validator