MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-qs Structured version   Unicode version

Definition df-qs 7354
Description: Define quotient set.  R is usually an equivalence relation. Definition of [Enderton] p. 58. (Contributed by NM, 23-Jul-1995.)
Assertion
Ref Expression
df-qs  |-  ( A /. R )  =  { y  |  E. x  e.  A  y  =  [ x ] R }
Distinct variable groups:    x, y, A    x, R, y

Detailed syntax breakdown of Definition df-qs
StepHypRef Expression
1 cA . . 3  class  A
2 cR . . 3  class  R
31, 2cqs 7347 . 2  class  ( A /. R )
4 vy . . . . . 6  setvar  y
54cv 1404 . . . . 5  class  y
6 vx . . . . . . 7  setvar  x
76cv 1404 . . . . . 6  class  x
87, 2cec 7346 . . . . 5  class  [ x ] R
95, 8wceq 1405 . . . 4  wff  y  =  [ x ] R
109, 6, 1wrex 2755 . . 3  wff  E. x  e.  A  y  =  [ x ] R
1110, 4cab 2387 . 2  class  { y  |  E. x  e.  A  y  =  [
x ] R }
123, 11wceq 1405 1  wff  ( A /. R )  =  { y  |  E. x  e.  A  y  =  [ x ] R }
Colors of variables: wff setvar class
This definition is referenced by:  qseq1  7398  qseq2  7399  elqsg  7400  qsexg  7406  uniqs  7408  snec  7411  qsinxp  7424  qliftf  7436  quslem  15157  pi1xfrf  21845  pi1cof  21851
  Copyright terms: Public domain W3C validator