Definition df-qs 8145

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 8138	. 2 class (𝐴 / 𝑅)
4		vy	. . . . . 6 setvar 𝑦
5	4	cv 1521	. . . . 5 class 𝑦
6		vx	. . . . . . 7 setvar 𝑥
7	6	cv 1521	. . . . . 6 class 𝑥
8	7, 2	cec 8137	. . . . 5 class [𝑥]𝑅
9	5, 8	wceq 1522	. . . 4 wff 𝑦 = [𝑥]𝑅
10	9, 6, 1	wrex 3106	. . 3 wff ∃𝑥 ∈ 𝐴 𝑦 = [𝑥]𝑅
11	10, 4	cab 2775	. 2 class {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = [𝑥]𝑅}
12	3, 11	wceq 1522	1 wff (𝐴 / 𝑅) = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = [𝑥]𝑅}

This definition is referenced by:  qseq1  8193  qseq2  8194  elqsg  8198  qsexg  8205  uniqs  8207  snec  8210  qsinxp  8223  qliftf  8235  quslem  16645  pi1xfrf  23340  pi1cof  23346  qsss1  35077  qsresid  35114  uniqsALTV  35118  0qs  35153  dfqs2  38652  dfqs3  38653