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=\left\{y|\exists x\in Ay=\left[x\right]R\right\}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	$$classA$$
1		cR	$$classR$$
2	0 1	cqs	$$class\left(A/R\right)$$
3		vy	$$setvary$$
4		vx	$$setvarx$$
5	3	cv	$$setvary$$
6	4	cv	$$setvarx$$
7	6 1	cec	$$class\left[x\right]R$$
8	5 7	wceq	$$wffy=\left[x\right]R$$
9	8 4 0	wrex	$$wff\exists x\in Ay=\left[x\right]R$$
10	9 3	cab	$$class\left\{y|\exists x\in Ay=\left[x\right]R\right\}$$
11	2 10	wceq	$$wffA/R=\left\{y|\exists x\in Ay=\left[x\right]R\right\}$$