Definition df-qs 8637

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

This definition is referenced by:  qseq1  8690  qseq2  8691  0qs  8696  elqsg  8697  qsexg  8705  uniqs  8707  snec  8711  qsinxp  8726  qliftf  8738  quslem  17455  qus0subgbas  19118  pzriprnglem11  21437  pi1xfrf  25000  pi1cof  25006  qusbas2  33415  qsss1  38400  qsresid  38436  qseq  38819  disjdmqscossss  38974  dfqs2  42408  dfqs3  42409