Definition df-qs 8696

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 8689	. 2 class (𝐴 / 𝑅)
4		vy	. . . . . 6 setvar 𝑦
5	4	cv 1566	. . . . 5 class 𝑦
6		vx	. . . . . . 7 setvar 𝑥
7	6	cv 1566	. . . . . 6 class 𝑥
8	7, 2	cec 8688	. . . . 5 class [𝑥]𝑅
9	5, 8	wceq 1567	. . . 4 wff 𝑦 = [𝑥]𝑅
10	9, 6, 1	wrex 3095	. . 3 wff ∃𝑥 ∈ 𝐴 𝑦 = [𝑥]𝑅
11	10, 4	cab 2747	. 2 class {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = [𝑥]𝑅}
12	3, 11	wceq 1567	1 wff (𝐴 / 𝑅) = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = [𝑥]𝑅}

This definition is referenced by:  dfqs2  8697  qseq1  8750  qseq2  8751  0qs  8756  elqsg  8757  qsexg  8765  uniqs  8767  snecg  8771  snec  8772  qsinxp  8787  qliftf  8799  quslem  17593  qus0subgbas  19265  pzriprnglem11  21606  pi1xfrf  25177  pi1cof  25183  qusbas2  33655  qsss1  38829  qsresid  38865  raldmqsmo  38897  qseq  39267  disjdmqscossss  39440  dfqs3  42890