Definition df-qs 8702

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 8695	. 2 class (𝐴 / 𝑅)
4		vy	. . . . . 6 setvar 𝑦
5	4	cv 1569	. . . . 5 class 𝑦
6		vx	. . . . . . 7 setvar 𝑥
7	6	cv 1569	. . . . . 6 class 𝑥
8	7, 2	cec 8694	. . . . 5 class [𝑥]𝑅
9	5, 8	wceq 1570	. . . 4 wff 𝑦 = [𝑥]𝑅
10	9, 6, 1	wrex 3091	. . 3 wff ∃𝑥 ∈ 𝐴 𝑦 = [𝑥]𝑅
11	10, 4	cab 2743	. 2 class {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = [𝑥]𝑅}
12	3, 11	wceq 1570	1 wff (𝐴 / 𝑅) = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = [𝑥]𝑅}

This definition is used by:  dfqs2  8703  qseq1  8756  qseq2  8757  0qs  8762  elqsg  8763  qsexg  8771  uniqs  8773  snecg  8777  snec  8778  qsinxp  8793  qliftf  8805  quslem  17614  qus0subgbas  19292  pzriprnglem11  21670  pi1xfrf  25241  pi1cof  25247  qusbas2  33738  qsss1  38977  qsresid  39013  raldmqsmo  39045  qseq  39415  disjdmqscossss  39588  dfqs3  43040