Definition df-qs 8628

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

This definition is referenced by:  qseq1  8681  qseq2  8682  0qs  8687  elqsg  8688  qsexg  8696  uniqs  8698  snec  8702  qsinxp  8717  qliftf  8729  quslem  17447  qus0subgbas  19111  pzriprnglem11  21429  pi1xfrf  24981  pi1cof  24987  qusbas2  33369  qsss1  38329  qsresid  38365  qseq  38692  disjdmqscossss  38847  dfqs2  42276  dfqs3  42277