Definition df-qs 8678

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 8671	. 2 class (𝐴 / 𝑅)
4		vy	. . . . . 6 setvar 𝑦
5	4	cv 1558	. . . . 5 class 𝑦
6		vx	. . . . . . 7 setvar 𝑥
7	6	cv 1558	. . . . . 6 class 𝑥
8	7, 2	cec 8670	. . . . 5 class [𝑥]𝑅
9	5, 8	wceq 1559	. . . 4 wff 𝑦 = [𝑥]𝑅
10	9, 6, 1	wrex 3085	. . 3 wff ∃𝑥 ∈ 𝐴 𝑦 = [𝑥]𝑅
11	10, 4	cab 2739	. 2 class {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = [𝑥]𝑅}
12	3, 11	wceq 1559	1 wff (𝐴 / 𝑅) = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = [𝑥]𝑅}

This definition is referenced by:  dfqs2  8679  qseq1  8732  qseq2  8733  0qs  8738  elqsg  8739  qsexg  8747  uniqs  8749  snecg  8753  snec  8754  qsinxp  8769  qliftf  8781  quslem  17564  qus0subgbas  19230  pzriprnglem11  21531  pi1xfrf  25103  pi1cof  25109  qusbas2  33553  qsss1  38755  qsresid  38791  raldmqsmo  38823  qseq  39193  disjdmqscossss  39366  dfqs3  42816