Definition df-qs 8701

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

This definition is referenced by:  dfqs2  8702  qseq1  8755  qseq2  8756  0qs  8761  elqsg  8762  qsexg  8770  uniqs  8772  snecg  8776  snec  8777  qsinxp  8792  qliftf  8804  quslem  17598  qus0subgbas  19270  pzriprnglem11  21622  pi1xfrf  25193  pi1cof  25199  qusbas2  33696  qsss1  38925  qsresid  38961  raldmqsmo  38993  qseq  39363  disjdmqscossss  39536  dfqs3  42988