Definition df-qs 8677

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 8670	. 2 class (𝐴 / 𝑅)
4		vy	. . . . . 6 setvar 𝑦
5	4	cv 1539	. . . . 5 class 𝑦
6		vx	. . . . . . 7 setvar 𝑥
7	6	cv 1539	. . . . . 6 class 𝑥
8	7, 2	cec 8669	. . . . 5 class [𝑥]𝑅
9	5, 8	wceq 1540	. . . 4 wff 𝑦 = [𝑥]𝑅
10	9, 6, 1	wrex 3053	. . 3 wff ∃𝑥 ∈ 𝐴 𝑦 = [𝑥]𝑅
11	10, 4	cab 2707	. 2 class {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = [𝑥]𝑅}
12	3, 11	wceq 1540	1 wff (𝐴 / 𝑅) = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = [𝑥]𝑅}

This definition is referenced by:  qseq1  8730  qseq2  8731  0qs  8736  elqsg  8737  qsexg  8745  uniqs  8747  snec  8751  qsinxp  8766  qliftf  8778  quslem  17506  qus0subgbas  19130  pzriprnglem11  21401  pi1xfrf  24953  pi1cof  24959  qusbas2  33377  qsss1  38277  qsresid  38313  qseq  38640  disjdmqscossss  38795  dfqs2  42225  dfqs3  42226