Definition df-qs 8751

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

This definition is referenced by:  qseq1  8801  qseq2  8802  0qs  8807  elqsg  8808  qsexg  8815  uniqs  8817  snec  8820  qsinxp  8833  qliftf  8845  quslem  17588  qus0subgbas  19216  pzriprnglem11  21502  pi1xfrf  25086  pi1cof  25092  qusbas2  33434  qsss1  38290  qsresid  38326  uniqsALTV  38330  disjdmqscossss  38804  dfqs2  42278  dfqs3  42279