![]() |
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 8138 | . 2 class (𝐴 / 𝑅) |
4 | vy | . . . . . 6 setvar 𝑦 | |
5 | 4 | cv 1521 | . . . . 5 class 𝑦 |
6 | vx | . . . . . . 7 setvar 𝑥 | |
7 | 6 | cv 1521 | . . . . . 6 class 𝑥 |
8 | 7, 2 | cec 8137 | . . . . 5 class [𝑥]𝑅 |
9 | 5, 8 | wceq 1522 | . . . 4 wff 𝑦 = [𝑥]𝑅 |
10 | 9, 6, 1 | wrex 3106 | . . 3 wff ∃𝑥 ∈ 𝐴 𝑦 = [𝑥]𝑅 |
11 | 10, 4 | cab 2775 | . 2 class {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = [𝑥]𝑅} |
12 | 3, 11 | wceq 1522 | 1 wff (𝐴 / 𝑅) = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = [𝑥]𝑅} |
Colors of variables: wff setvar class |
This definition is referenced by: qseq1 8193 qseq2 8194 elqsg 8198 qsexg 8205 uniqs 8207 snec 8210 qsinxp 8223 qliftf 8235 quslem 16645 pi1xfrf 23340 pi1cof 23346 qsss1 35077 qsresid 35114 uniqsALTV 35118 0qs 35153 dfqs2 38652 dfqs3 38653 |
Copyright terms: Public domain | W3C validator |