Definition df-qs 8702

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 8695	. 2 class (𝐴 / 𝑅)
4		vy	. . . . . 6 setvar 𝑦
5	4	cv 1569	. . . . 5 class 𝑦
6		vx	. . . . . . 7 setvar 𝑥
7	6	cv 1569	. . . . . 6 class 𝑥
8	7, 2	cec 8694	. . . . 5 class [𝑥]𝑅
9	5, 8	wceq 1570	. . . 4 wff 𝑦 = [𝑥]𝑅
10	9, 6, 1	wrex 3086	. . 3 wff ∃𝑥 ∈ 𝐴 𝑦 = [𝑥]𝑅
11	10, 4	cab 2738	. 2 class {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = [𝑥]𝑅}
12	3, 11	wceq 1570	1 wff (𝐴 / 𝑅) = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = [𝑥]𝑅}

This definition is used by:  dfqs2  8703  qseq1  8756  qseq2  8757  0qs  8762  elqsg  8763  qsexg  8771  uniqs  8773  snecg  8777  snec  8778  qsinxp  8793  qliftf  8805  quslem  17629  qus0subgbas  19326  pzriprnglem11  21704  pi1xfrf  25281  pi1cof  25287  qusbas2  33835  qsss1  39043  qsresid  39079  raldmqsmo  39111  qseq  39481  disjdmqscossss  39654  dfqs3  43106