| 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 8744 | . 2 class (𝐴 / 𝑅) |
| 4 | vy | . . . . . 6 setvar 𝑦 | |
| 5 | 4 | cv 1539 | . . . . 5 class 𝑦 |
| 6 | vx | . . . . . . 7 setvar 𝑥 | |
| 7 | 6 | cv 1539 | . . . . . 6 class 𝑥 |
| 8 | 7, 2 | cec 8743 | . . . . 5 class [𝑥]𝑅 |
| 9 | 5, 8 | wceq 1540 | . . . 4 wff 𝑦 = [𝑥]𝑅 |
| 10 | 9, 6, 1 | wrex 3070 | . . 3 wff ∃𝑥 ∈ 𝐴 𝑦 = [𝑥]𝑅 |
| 11 | 10, 4 | cab 2714 | . 2 class {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = [𝑥]𝑅} |
| 12 | 3, 11 | wceq 1540 | 1 wff (𝐴 / 𝑅) = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = [𝑥]𝑅} |
| Colors of variables: wff setvar class |
| This definition is referenced by: qseq1 8801 qseq2 8802 0qs 8807 elqsg 8808 qsexg 8815 uniqs 8817 snec 8820 qsinxp 8833 qliftf 8845 quslem 17588 qus0subgbas 19216 pzriprnglem11 21502 pi1xfrf 25086 pi1cof 25092 qusbas2 33434 qsss1 38290 qsresid 38326 uniqsALTV 38330 disjdmqscossss 38804 dfqs2 42278 dfqs3 42279 |
| Copyright terms: Public domain | W3C validator |