Metamath Proof Explorer

Definition df-qs

Description: Define quotient set. R is usually an equivalence relation. Definition of Enderton p. 58. (Contributed by NM, 23-Jul-1995)

Ref Expression
Assertion df-qs 
|- ( A /. R ) = { y | E. x e. A y = [ x ] R }

Detailed syntax breakdown

Step Hyp Ref Expression
0 cA 
 |-  A
1 cR 
 |-  R
2 0 1 cqs 
 |-  ( A /. R )
3 vy 
 |-  y
4 vx 
 |-  x
5 3 cv 
 |-  y
6 4 cv 
 |-  x
7 6 1 cec 
 |-  [ x ] R
8 5 7 wceq 
 |-  y = [ x ] R
9 8 4 0 wrex 
 |-  E. x e. A y = [ x ] R
10 9 3 cab 
 |-  { y | E. x e. A y = [ x ] R }
11 2 10 wceq 
 |-  ( A /. R ) = { y | E. x e. A y = [ x ] R }