Definition df-qs 8628

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

This definition is referenced by:  qseq1  8681  qseq2  8682  0qs  8687  elqsg  8688  qsexg  8696  uniqs  8698  snec  8702  qsinxp  8717  qliftf  8729  quslem  17447  qus0subgbas  19110  pzriprnglem11  21428  pi1xfrf  24980  pi1cof  24986  qusbas2  33371  qsss1  38326  qsresid  38362  qseq  38745  disjdmqscossss  38900  dfqs2  42329  dfqs3  42330