Definition df-qs 8651

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

Step	Hyp	Ref	Expression
1		cA	. . 3 class 𝐴
2		cR	. . 3 class 𝑅
3	1, 2	cqs 8644	. 2 class (𝐴 / 𝑅)
4		vy	. . . . . 6 setvar 𝑦
5	4	cv 1541	. . . . 5 class 𝑦
6		vx	. . . . . . 7 setvar 𝑥
7	6	cv 1541	. . . . . 6 class 𝑥
8	7, 2	cec 8643	. . . . 5 class [𝑥]𝑅
9	5, 8	wceq 1542	. . . 4 wff 𝑦 = [𝑥]𝑅
10	9, 6, 1	wrex 3062	. . 3 wff ∃𝑥 ∈ 𝐴 𝑦 = [𝑥]𝑅
11	10, 4	cab 2715	. 2 class {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = [𝑥]𝑅}
12	3, 11	wceq 1542	1 wff (𝐴 / 𝑅) = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = [𝑥]𝑅}

This definition is referenced by:  dfqs2  8652  qseq1  8705  qseq2  8706  0qs  8711  elqsg  8712  qsexg  8720  uniqs  8722  snecg  8726  snec  8727  qsinxp  8742  qliftf  8754  quslem  17476  qus0subgbas  19139  pzriprnglem11  21458  pi1xfrf  25021  pi1cof  25027  qusbas2  33498  qsss1  38543  qsresid  38579  raldmqsmo  38611  qseq  38981  disjdmqscossss  39154  dfqs3  42606