Definition df-qs 8769

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

This definition is referenced by:  qseq1  8819  qseq2  8820  0qs  8825  elqsg  8826  qsexg  8833  uniqs  8835  snec  8838  qsinxp  8851  qliftf  8863  quslem  17603  qus0subgbas  19238  pzriprnglem11  21525  pi1xfrf  25105  pi1cof  25111  qusbas2  33399  qsss1  38245  qsresid  38281  uniqsALTV  38285  disjdmqscossss  38759  dfqs2  42232  dfqs3  42233