Definition df-qs 8705

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

This definition is referenced by:  qseq1  8753  qseq2  8754  elqsg  8758  qsexg  8765  uniqs  8767  snec  8770  qsinxp  8783  qliftf  8795  quslem  17485  qus0subgbas  19069  pi1xfrf  24551  pi1cof  24557  qsss1  37095  qsresid  37132  uniqsALTV  37136  0qs  37177  disjdmqscossss  37611  dfqs2  41008  dfqs3  41009