Definition df-qs 8649

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 8642	. 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 8641	. . . . 5 class [𝑥]𝑅
9	5, 8	wceq 1542	. . . 4 wff 𝑦 = [𝑥]𝑅
10	9, 6, 1	wrex 3061	. . 3 wff ∃𝑥 ∈ 𝐴 𝑦 = [𝑥]𝑅
11	10, 4	cab 2714	. 2 class {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = [𝑥]𝑅}
12	3, 11	wceq 1542	1 wff (𝐴 / 𝑅) = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = [𝑥]𝑅}

This definition is referenced by:  dfqs2  8650  qseq1  8703  qseq2  8704  0qs  8709  elqsg  8710  qsexg  8718  uniqs  8720  snecg  8724  snec  8725  qsinxp  8740  qliftf  8752  quslem  17507  qus0subgbas  19173  pzriprnglem11  21471  pi1xfrf  25020  pi1cof  25026  qusbas2  33466  qsss1  38616  qsresid  38652  raldmqsmo  38684  qseq  39054  disjdmqscossss  39227  dfqs3  42678