Definition df-qs 8749

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 8742	. 2 class (𝐴 / 𝑅)
4		vy	. . . . . 6 setvar 𝑦
5	4	cv 1535	. . . . 5 class 𝑦
6		vx	. . . . . . 7 setvar 𝑥
7	6	cv 1535	. . . . . 6 class 𝑥
8	7, 2	cec 8741	. . . . 5 class [𝑥]𝑅
9	5, 8	wceq 1536	. . . 4 wff 𝑦 = [𝑥]𝑅
10	9, 6, 1	wrex 3067	. . 3 wff ∃𝑥 ∈ 𝐴 𝑦 = [𝑥]𝑅
11	10, 4	cab 2711	. 2 class {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = [𝑥]𝑅}
12	3, 11	wceq 1536	1 wff (𝐴 / 𝑅) = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = [𝑥]𝑅}

This definition is referenced by:  qseq1  8799  qseq2  8800  0qs  8805  elqsg  8806  qsexg  8813  uniqs  8815  snec  8818  qsinxp  8831  qliftf  8843  quslem  17589  qus0subgbas  19228  pzriprnglem11  21519  pi1xfrf  25099  pi1cof  25105  qusbas2  33413  qsss1  38270  qsresid  38306  uniqsALTV  38310  disjdmqscossss  38784  dfqs2  42256  dfqs3  42257