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

Definition df-qs 6019
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 (A / 𝑅) = {yx A y = [x]𝑅}
Distinct variable groups:   x,y,A   x,𝑅,y

Detailed syntax breakdown of Definition df-qs
StepHypRef Expression
1 cA . . 3 class A
2 cR . . 3 class 𝑅
31, 2cqs 6012 . 2 class (A / 𝑅)
4 vy . . . . . 6 setvar y
54cv 1225 . . . . 5 class y
6 vx . . . . . . 7 setvar x
76cv 1225 . . . . . 6 class x
87, 2cec 6011 . . . . 5 class [x]𝑅
95, 8wceq 1226 . . . 4 wff y = [x]𝑅
109, 6, 1wrex 2281 . . 3 wff x A y = [x]𝑅
1110, 4cab 2004 . 2 class {yx A y = [x]𝑅}
123, 11wceq 1226 1 wff (A / 𝑅) = {yx A y = [x]𝑅}
Colors of variables: wff set class
This definition is referenced by:  qseq1  6061  qseq2  6062  elqsg  6063  qsexg  6069  uniqs  6071  snec  6074  qsinxp  6089  qliftf  6098
  Copyright terms: Public domain W3C validator