![]() |
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 8733 | . 2 class (𝐴 / 𝑅) |
4 | vy | . . . . . 6 setvar 𝑦 | |
5 | 4 | cv 1533 | . . . . 5 class 𝑦 |
6 | vx | . . . . . . 7 setvar 𝑥 | |
7 | 6 | cv 1533 | . . . . . 6 class 𝑥 |
8 | 7, 2 | cec 8732 | . . . . 5 class [𝑥]𝑅 |
9 | 5, 8 | wceq 1534 | . . . 4 wff 𝑦 = [𝑥]𝑅 |
10 | 9, 6, 1 | wrex 3060 | . . 3 wff ∃𝑥 ∈ 𝐴 𝑦 = [𝑥]𝑅 |
11 | 10, 4 | cab 2703 | . 2 class {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = [𝑥]𝑅} |
12 | 3, 11 | wceq 1534 | 1 wff (𝐴 / 𝑅) = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = [𝑥]𝑅} |
Colors of variables: wff setvar class |
This definition is referenced by: qseq1 8790 qseq2 8791 0qs 8796 elqsg 8797 qsexg 8804 uniqs 8806 snec 8809 qsinxp 8822 qliftf 8834 quslem 17558 qus0subgbas 19192 pzriprnglem11 21481 pi1xfrf 25071 pi1cof 25077 qusbas2 33281 qsss1 37987 qsresid 38023 uniqsALTV 38027 disjdmqscossss 38501 dfqs2 41961 dfqs3 41962 |
Copyright terms: Public domain | W3C validator |