Definition df-qs 8641

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

This definition is referenced by:  qseq1  8694  qseq2  8695  0qs  8700  elqsg  8701  qsexg  8709  uniqs  8711  snec  8715  qsinxp  8730  qliftf  8742  quslem  17464  qus0subgbas  19127  pzriprnglem11  21446  pi1xfrf  25009  pi1cof  25015  qusbas2  33487  qsss1  38488  qsresid  38524  qseq  38907  disjdmqscossss  39062  dfqs2  42493  dfqs3  42494