Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > df-qs | Structured version Visualization version GIF version |
Description: Define quotient set. 𝑅 is usually an equivalence relation. Definition of [Enderton] p. 58. (Contributed by NM, 23-Jul-1995.) |
Ref | Expression |
---|---|
df-qs | ⊢ (𝐴 / 𝑅) = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = [𝑥]𝑅} |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cA | . . 3 class 𝐴 | |
2 | cR | . . 3 class 𝑅 | |
3 | 1, 2 | cqs 8278 | . 2 class (𝐴 / 𝑅) |
4 | vy | . . . . . 6 setvar 𝑦 | |
5 | 4 | cv 1527 | . . . . 5 class 𝑦 |
6 | vx | . . . . . . 7 setvar 𝑥 | |
7 | 6 | cv 1527 | . . . . . 6 class 𝑥 |
8 | 7, 2 | cec 8277 | . . . . 5 class [𝑥]𝑅 |
9 | 5, 8 | wceq 1528 | . . . 4 wff 𝑦 = [𝑥]𝑅 |
10 | 9, 6, 1 | wrex 3139 | . . 3 wff ∃𝑥 ∈ 𝐴 𝑦 = [𝑥]𝑅 |
11 | 10, 4 | cab 2799 | . 2 class {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = [𝑥]𝑅} |
12 | 3, 11 | wceq 1528 | 1 wff (𝐴 / 𝑅) = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = [𝑥]𝑅} |
Colors of variables: wff setvar class |
This definition is referenced by: qseq1 8333 qseq2 8334 elqsg 8338 qsexg 8345 uniqs 8347 snec 8350 qsinxp 8363 qliftf 8375 quslem 16806 pi1xfrf 23586 pi1cof 23592 qsss1 35428 qsresid 35465 uniqsALTV 35469 0qs 35504 dfqs2 39002 dfqs3 39003 |
Copyright terms: Public domain | W3C validator |