| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > df-opab | Structured version Visualization version GIF version | ||
| Description: Define the class abstraction of a collection of ordered pairs. Definition 3.3 of [Monk1] p. 34. Usually 𝑥 and 𝑦 are distinct, although the definition does not require it (see dfid2 5580 for a case where they are not distinct). The brace notation is called "class abstraction" by Quine; it is also called "class builder" in the literature. An alternate definition using no existential quantifiers is shown by dfopab2 8077. An example is given by ex-opab 30451. (Contributed by NM, 4-Jul-1994.) |
| Ref | Expression |
|---|---|
| df-opab | ⊢ {〈𝑥, 𝑦〉 ∣ 𝜑} = {𝑧 ∣ ∃𝑥∃𝑦(𝑧 = 〈𝑥, 𝑦〉 ∧ 𝜑)} |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | wph | . . 3 wff 𝜑 | |
| 2 | vx | . . 3 setvar 𝑥 | |
| 3 | vy | . . 3 setvar 𝑦 | |
| 4 | 1, 2, 3 | copab 5205 | . 2 class {〈𝑥, 𝑦〉 ∣ 𝜑} |
| 5 | vz | . . . . . . . 8 setvar 𝑧 | |
| 6 | 5 | cv 1539 | . . . . . . 7 class 𝑧 |
| 7 | 2 | cv 1539 | . . . . . . . 8 class 𝑥 |
| 8 | 3 | cv 1539 | . . . . . . . 8 class 𝑦 |
| 9 | 7, 8 | cop 4632 | . . . . . . 7 class 〈𝑥, 𝑦〉 |
| 10 | 6, 9 | wceq 1540 | . . . . . 6 wff 𝑧 = 〈𝑥, 𝑦〉 |
| 11 | 10, 1 | wa 395 | . . . . 5 wff (𝑧 = 〈𝑥, 𝑦〉 ∧ 𝜑) |
| 12 | 11, 3 | wex 1779 | . . . 4 wff ∃𝑦(𝑧 = 〈𝑥, 𝑦〉 ∧ 𝜑) |
| 13 | 12, 2 | wex 1779 | . . 3 wff ∃𝑥∃𝑦(𝑧 = 〈𝑥, 𝑦〉 ∧ 𝜑) |
| 14 | 13, 5 | cab 2714 | . 2 class {𝑧 ∣ ∃𝑥∃𝑦(𝑧 = 〈𝑥, 𝑦〉 ∧ 𝜑)} |
| 15 | 4, 14 | wceq 1540 | 1 wff {〈𝑥, 𝑦〉 ∣ 𝜑} = {𝑧 ∣ ∃𝑥∃𝑦(𝑧 = 〈𝑥, 𝑦〉 ∧ 𝜑)} |
| Colors of variables: wff setvar class |
| This definition is referenced by: opabss 5207 opabbid 5208 opabbidv 5209 nfopabd 5211 nfopab1 5213 nfopab2 5214 cbvopab 5215 cbvopabv 5216 cbvopab1 5217 cbvopab1g 5218 cbvopab2 5219 cbvopab1s 5220 cbvopab1v 5221 cbvopab2v 5223 unopab 5224 opabidw 5529 opabid 5530 elopabw 5531 ssopab2 5551 iunopab 5564 iunopabOLD 5565 dfid2 5580 dfid3 5581 elxpi 5707 opabssxpd 5732 rabxp 5733 csbxp 5785 ssrelOLD 5793 relopabi 5832 relopabiALT 5833 cnv0 6160 dfoprab2 7491 dmoprab 7536 dfopab2 8077 brdom7disj 10571 brdom6disj 10572 opabssi 32625 cbvopab1davw 36265 cbvopab2davw 36266 cbvopabdavw 36267 bj-dfid2ALT 37066 rnxrn 38399 dropab1 44466 dropab2 44467 csbxpgVD 44914 relopabVD 44921 |
| Copyright terms: Public domain | W3C validator |