Definition df-qs 8375

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 8368	. 2 class (𝐴 / 𝑅)
4		vy	. . . . . 6 setvar 𝑦
5	4	cv 1542	. . . . 5 class 𝑦
6		vx	. . . . . . 7 setvar 𝑥
7	6	cv 1542	. . . . . 6 class 𝑥
8	7, 2	cec 8367	. . . . 5 class [𝑥]𝑅
9	5, 8	wceq 1543	. . . 4 wff 𝑦 = [𝑥]𝑅
10	9, 6, 1	wrex 3052	. . 3 wff ∃𝑥 ∈ 𝐴 𝑦 = [𝑥]𝑅
11	10, 4	cab 2714	. 2 class {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = [𝑥]𝑅}
12	3, 11	wceq 1543	1 wff (𝐴 / 𝑅) = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = [𝑥]𝑅}

This definition is referenced by:  qseq1  8423  qseq2  8424  elqsg  8428  qsexg  8435  uniqs  8437  snec  8440  qsinxp  8453  qliftf  8465  quslem  17002  pi1xfrf  23904  pi1cof  23910  qsss1  36109  qsresid  36146  uniqsALTV  36150  0qs  36186  dfqs2  39866  dfqs3  39867