Definition df-qs 8677

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 8670	. 2 class (𝐴 / 𝑅)
4		vy	. . . . . 6 setvar 𝑦
5	4	cv 1558	. . . . 5 class 𝑦
6		vx	. . . . . . 7 setvar 𝑥
7	6	cv 1558	. . . . . 6 class 𝑥
8	7, 2	cec 8669	. . . . 5 class [𝑥]𝑅
9	5, 8	wceq 1559	. . . 4 wff 𝑦 = [𝑥]𝑅
10	9, 6, 1	wrex 3085	. . 3 wff ∃𝑥 ∈ 𝐴 𝑦 = [𝑥]𝑅
11	10, 4	cab 2739	. 2 class {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = [𝑥]𝑅}
12	3, 11	wceq 1559	1 wff (𝐴 / 𝑅) = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = [𝑥]𝑅}

This definition is referenced by:  dfqs2  8678  qseq1  8731  qseq2  8732  0qs  8737  elqsg  8738  qsexg  8746  uniqs  8748  snecg  8752  snec  8753  qsinxp  8768  qliftf  8780  quslem  17563  qus0subgbas  19229  pzriprnglem11  21530  pi1xfrf  25102  pi1cof  25108  qusbas2  33552  qsss1  38754  qsresid  38790  raldmqsmo  38822  qseq  39192  disjdmqscossss  39365  dfqs3  42815