| 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 8670 | . 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 8669 | . . . . 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 (𝐴 / 𝑅) = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = [𝑥]𝑅} |
| Colors of variables: wff setvar class |
| This definition is referenced by: dfqs2 8678 qseq1 8731 qseq2 8732 0qs 8737 elqsg 8738 qsexg 8746 uniqs 8748 snecg 8752 snec 8753 qsinxp 8768 qliftf 8780 quslem 17563 qus0subgbas 19229 pzriprnglem11 21530 pi1xfrf 25102 pi1cof 25108 qusbas2 33552 qsss1 38754 qsresid 38790 raldmqsmo 38822 qseq 39192 disjdmqscossss 39365 dfqs3 42815 |
| Copyright terms: Public domain | W3C validator |