Definition df-qs 8740

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 8733	. 2 class (𝐴 / 𝑅)
4		vy	. . . . . 6 setvar 𝑦
5	4	cv 1533	. . . . 5 class 𝑦
6		vx	. . . . . . 7 setvar 𝑥
7	6	cv 1533	. . . . . 6 class 𝑥
8	7, 2	cec 8732	. . . . 5 class [𝑥]𝑅
9	5, 8	wceq 1534	. . . 4 wff 𝑦 = [𝑥]𝑅
10	9, 6, 1	wrex 3060	. . 3 wff ∃𝑥 ∈ 𝐴 𝑦 = [𝑥]𝑅
11	10, 4	cab 2703	. 2 class {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = [𝑥]𝑅}
12	3, 11	wceq 1534	1 wff (𝐴 / 𝑅) = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = [𝑥]𝑅}

This definition is referenced by:  qseq1  8790  qseq2  8791  0qs  8796  elqsg  8797  qsexg  8804  uniqs  8806  snec  8809  qsinxp  8822  qliftf  8834  quslem  17558  qus0subgbas  19192  pzriprnglem11  21481  pi1xfrf  25071  pi1cof  25077  qusbas2  33281  qsss1  37987  qsresid  38023  uniqsALTV  38027  disjdmqscossss  38501  dfqs2  41961  dfqs3  41962