Definition df-qs 8642

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

This definition is referenced by:  dfqs2  8643  qseq1  8696  qseq2  8697  0qs  8702  elqsg  8703  qsexg  8711  uniqs  8713  snecg  8717  snec  8718  qsinxp  8733  qliftf  8745  quslem  17498  qus0subgbas  19164  pzriprnglem11  21481  pi1xfrf  25030  pi1cof  25036  qusbas2  33481  qsss1  38630  qsresid  38666  raldmqsmo  38698  qseq  39068  disjdmqscossss  39241  dfqs3  42692