Definition df-qs 8504

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

This definition is referenced by:  qseq1  8552  qseq2  8553  elqsg  8557  qsexg  8564  uniqs  8566  snec  8569  qsinxp  8582  qliftf  8594  quslem  17254  pi1xfrf  24216  pi1cof  24222  qsss1  36423  qsresid  36460  uniqsALTV  36464  0qs  36500  dfqs2  40212  dfqs3  40213