Definition df-qs 8646

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 8639	. 2 class (𝐴 / 𝑅)
4		vy	. . . . . 6 setvar 𝑦
5	4	cv 1546	. . . . 5 class 𝑦
6		vx	. . . . . . 7 setvar 𝑥
7	6	cv 1546	. . . . . 6 class 𝑥
8	7, 2	cec 8638	. . . . 5 class [𝑥]𝑅
9	5, 8	wceq 1547	. . . 4 wff 𝑦 = [𝑥]𝑅
10	9, 6, 1	wrex 3064	. . 3 wff ∃𝑥 ∈ 𝐴 𝑦 = [𝑥]𝑅
11	10, 4	cab 2718	. 2 class {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = [𝑥]𝑅}
12	3, 11	wceq 1547	1 wff (𝐴 / 𝑅) = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = [𝑥]𝑅}

This definition is referenced by:  dfqs2  8647  qseq1  8700  qseq2  8701  0qs  8706  elqsg  8707  qsexg  8715  uniqs  8717  snecg  8721  snec  8722  qsinxp  8737  qliftf  8749  quslem  17505  qus0subgbas  19171  pzriprnglem11  21473  pi1xfrf  25045  pi1cof  25051  qusbas2  33496  qsss1  38669  qsresid  38705  raldmqsmo  38737  qseq  39107  disjdmqscossss  39280  dfqs3  42730