Definition df-qs 8709

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 8702	. 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 8701	. . . . 5 class [𝑥]𝑅
9	5, 8	wceq 1542	. . . 4 wff 𝑦 = [𝑥]𝑅
10	9, 6, 1	wrex 3071	. . 3 wff ∃𝑥 ∈ 𝐴 𝑦 = [𝑥]𝑅
11	10, 4	cab 2710	. 2 class {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = [𝑥]𝑅}
12	3, 11	wceq 1542	1 wff (𝐴 / 𝑅) = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = [𝑥]𝑅}

This definition is referenced by:  qseq1  8757  qseq2  8758  elqsg  8762  qsexg  8769  uniqs  8771  snec  8774  qsinxp  8787  qliftf  8799  quslem  17489  qus0subgbas  19075  pi1xfrf  24569  pi1cof  24575  qusbas2  32517  qsss1  37157  qsresid  37194  uniqsALTV  37198  0qs  37239  disjdmqscossss  37673  dfqs2  41059  dfqs3  41060  pzriprnglem11  46815