Definition df-qs 8638

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 8631	. 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 8630	. . . . 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  8691  qseq2  8692  0qs  8697  elqsg  8698  qsexg  8706  uniqs  8708  snec  8712  qsinxp  8727  qliftf  8739  quslem  17465  qus0subgbas  19095  pzriprnglem11  21416  pi1xfrf  24969  pi1cof  24975  qusbas2  33356  qsss1  38265  qsresid  38301  qseq  38628  disjdmqscossss  38783  dfqs2  42213  dfqs3  42214