Definition df-qs 8680

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 8673	. 2 class (𝐴 / 𝑅)
4		vy	. . . . . 6 setvar 𝑦
5	4	cv 1539	. . . . 5 class 𝑦
6		vx	. . . . . . 7 setvar 𝑥
7	6	cv 1539	. . . . . 6 class 𝑥
8	7, 2	cec 8672	. . . . 5 class [𝑥]𝑅
9	5, 8	wceq 1540	. . . 4 wff 𝑦 = [𝑥]𝑅
10	9, 6, 1	wrex 3054	. . 3 wff ∃𝑥 ∈ 𝐴 𝑦 = [𝑥]𝑅
11	10, 4	cab 2708	. 2 class {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = [𝑥]𝑅}
12	3, 11	wceq 1540	1 wff (𝐴 / 𝑅) = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = [𝑥]𝑅}

This definition is referenced by:  qseq1  8733  qseq2  8734  0qs  8739  elqsg  8740  qsexg  8748  uniqs  8750  snec  8754  qsinxp  8769  qliftf  8781  quslem  17513  qus0subgbas  19137  pzriprnglem11  21408  pi1xfrf  24960  pi1cof  24966  qusbas2  33384  qsss1  38284  qsresid  38320  qseq  38647  disjdmqscossss  38802  dfqs2  42232  dfqs3  42233