Definition df-qs 8716

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 8709	. 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 8708	. . . . 5 class [𝑥]𝑅
9	5, 8	wceq 1570	. . . 4 wff 𝑦 = [𝑥]𝑅
10	9, 6, 1	wrex 3087	. . 3 wff ∃𝑥 ∈ 𝐴 𝑦 = [𝑥]𝑅
11	10, 4	cab 2739	. 2 class {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = [𝑥]𝑅}
12	3, 11	wceq 1570	1 wff (𝐴 / 𝑅) = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = [𝑥]𝑅}

This definition is used by:  dfqs2  8717  qseq1  8770  qseq2  8771  0qs  8776  elqsg  8777  qsexg  8785  uniqs  8787  snecg  8791  snec  8792  qsinxp  8807  qliftf  8819  quslem  17708  qus0subgbas  19406  pzriprnglem11  21790  pi1xfrf  25367  pi1cof  25373  qusbas2  33950  qsss1  39207  qsresid  39243  raldmqsmo  39275  qseq  39645  disjdmqscossss  39818  dfqs3  43270