Definition df-qs 8759

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 8752	. 2 class (𝐴 / 𝑅)
4		vy	. . . . . 6 setvar 𝑦
5	4	cv 1569	. . . . 5 class 𝑦
6		vx	. . . . . . 7 setvar 𝑥
7	6	cv 1569	. . . . . 6 class 𝑥
8	7, 2	cec 8751	. . . . 5 class [𝑥]𝑅
9	5, 8	wceq 1570	. . . 4 wff 𝑦 = [𝑥]𝑅
10	9, 6, 1	wrex 3090	. . 3 wff ∃𝑥 ∈ 𝐴 𝑦 = [𝑥]𝑅
11	10, 4	cab 2741	. 2 class {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = [𝑥]𝑅}
12	3, 11	wceq 1570	1 wff (𝐴 / 𝑅) = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = [𝑥]𝑅}

This definition is used by:  dfqs2  8760  qseq1  8813  qseq2  8814  0qs  8819  elqsg  8820  qsexg  8828  uniqs  8830  snecg  8834  snec  8835  qsinxp  8850  qliftf  8862  quslem  17756  qus0subgbas  19454  pzriprnglem11  21841  pi1xfrf  25418  pi1cof  25424  qusbas2  34054  qsss1  39486  qsresid  39522  raldmqsmo  39554  qseq  39924  disjdmqscossss  40097  dfqs3  43550