ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-qs Structured version   Unicode version

Definition df-qs 6011
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 
/. R  {  |  R }
Distinct variable groups:   ,,   , R,

Detailed syntax breakdown of Definition df-qs
StepHypRef Expression
1 cA . . 3
2 cR . . 3  R
31, 2cqs 6004 . 2 
/. R
4 vy . . . . . 6  setvar
54cv 1222 . . . . 5
6 vx . . . . . . 7  setvar
76cv 1222 . . . . . 6
87, 2cec 6003 . . . . 5  R
95, 8wceq 1223 . . . 4  R
109, 6, 1wrex 2276 . . 3  R
1110, 4cab 1999 . 2  {  |  R }
123, 11wceq 1223 1  /. R  {  |  R }
Colors of variables: wff set class
This definition is referenced by:  qseq1  6053  qseq2  6054  elqsg  6055  qsexg  6061  uniqs  6063  snec  6066  qsinxp  6081  qliftf  6090
  Copyright terms: Public domain W3C validator