Definition df-qs 8295

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 8288	. 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 8287	. . . . 5 class [𝑥]𝑅
9	5, 8	wceq 1537	. . . 4 wff 𝑦 = [𝑥]𝑅
10	9, 6, 1	wrex 3139	. . 3 wff ∃𝑥 ∈ 𝐴 𝑦 = [𝑥]𝑅
11	10, 4	cab 2799	. 2 class {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = [𝑥]𝑅}
12	3, 11	wceq 1537	1 wff (𝐴 / 𝑅) = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = [𝑥]𝑅}

This definition is referenced by:  qseq1  8343  qseq2  8344  elqsg  8348  qsexg  8355  uniqs  8357  snec  8360  qsinxp  8373  qliftf  8385  quslem  16816  pi1xfrf  23657  pi1cof  23663  qsss1  35560  qsresid  35597  uniqsALTV  35601  0qs  35637  dfqs2  39142  dfqs3  39143