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

Definition df-qs 7336
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
2 cR . . 3
31, 2cqs 7329 . 2
4 vy . . . . . 6
54cv 1394 . . . . 5
6 vx . . . . . . 7
76cv 1394 . . . . . 6
87, 2cec 7328 . . . . 5
95, 8wceq 1395 . . . 4
109, 6, 1wrex 2808 . . 3
1110, 4cab 2442 . 2
123, 11wceq 1395 1
Colors of variables: wff setvar class
This definition is referenced by:  qseq1  7380  qseq2  7381  elqsg  7382  qsexg  7388  uniqs  7390  snec  7393  qsinxp  7406  qliftf  7418  quslem  14940  pi1xfrf  21553  pi1cof  21559
  Copyright terms: Public domain W3C validator