New Foundations Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  NFE Home  >  Th. List  >  df-qs GIF version

Definition df-qs 5951
 Description: Define quotient set. R is usually an equivalence relation. Definition of [Enderton] p. 58. (Contributed by set.mm contributors, 22-Feb-2015.)
Assertion
Ref Expression
df-qs (A / R) = {y x 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 5946 . 2 class (A / R)
4 vy . . . . . 6 setvar y
54cv 1641 . . . . 5 class y
6 vx . . . . . . 7 setvar x
76cv 1641 . . . . . 6 class x
87, 2cec 5945 . . . . 5 class [x]R
95, 8wceq 1642 . . . 4 wff y = [x]R
109, 6, 1wrex 2615 . . 3 wff x A y = [x]R
1110, 4cab 2339 . 2 class {y x A y = [x]R}
123, 11wceq 1642 1 wff (A / R) = {y x A y = [x]R}
 Colors of variables: wff setvar class This definition is referenced by:  qseq1  5974  qseq2  5975  elqsg  5976  qsexg  5982  uniqs  5984  snec  5987
 Copyright terms: Public domain W3C validator