Definition df-qs 8727

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 8720	. 2 class (𝐴 / 𝑅)
4		vy	. . . . . 6 setvar 𝑦
5	4	cv 1568	. . . . 5 class 𝑦
6		vx	. . . . . . 7 setvar 𝑥
7	6	cv 1568	. . . . . 6 class 𝑥
8	7, 2	cec 8719	. . . . 5 class [𝑥]𝑅
9	5, 8	wceq 1569	. . . 4 wff 𝑦 = [𝑥]𝑅
10	9, 6, 1	wrex 3086	. . 3 wff ∃𝑥 ∈ 𝐴 𝑦 = [𝑥]𝑅
11	10, 4	cab 2738	. 2 class {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = [𝑥]𝑅}
12	3, 11	wceq 1569	1 wff (𝐴 / 𝑅) = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = [𝑥]𝑅}

This definition is used by:  dfqs2  8728  qseq1  8781  qseq2  8782  0qs  8787  elqsg  8788  qsexg  8796  uniqs  8798  snecg  8802  snec  8803  qsinxp  8818  qliftf  8830  quslem  17721  qus0subgbas  19419  pzriprnglem11  21803  pi1xfrf  25380  pi1cof  25386  qusbas2  34004  qsss1  39321  qsresid  39357  raldmqsmo  39389  qseq  39759  disjdmqscossss  39932  dfqs3  43384