Definition df-qs 8699

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 8692	. 2 class (𝐴 / 𝑅)
4		vy	. . . . . 6 setvar 𝑦
5	4	cv 1566	. . . . 5 class 𝑦
6		vx	. . . . . . 7 setvar 𝑥
7	6	cv 1566	. . . . . 6 class 𝑥
8	7, 2	cec 8691	. . . . 5 class [𝑥]𝑅
9	5, 8	wceq 1567	. . . 4 wff 𝑦 = [𝑥]𝑅
10	9, 6, 1	wrex 3095	. . 3 wff ∃𝑥 ∈ 𝐴 𝑦 = [𝑥]𝑅
11	10, 4	cab 2747	. 2 class {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = [𝑥]𝑅}
12	3, 11	wceq 1567	1 wff (𝐴 / 𝑅) = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = [𝑥]𝑅}

This definition is referenced by:  dfqs2  8700  qseq1  8753  qseq2  8754  0qs  8759  elqsg  8760  qsexg  8768  uniqs  8770  snecg  8774  snec  8775  qsinxp  8790  qliftf  8802  quslem  17596  qus0subgbas  19268  pzriprnglem11  21609  pi1xfrf  25180  pi1cof  25186  qusbas2  33658  qsss1  38833  qsresid  38869  raldmqsmo  38901  qseq  39271  disjdmqscossss  39444  dfqs3  42896