![]() |
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 doesn't strictly require it (see dfid2 5169 for a case where they are not distinct). The brace notation is called "class abstraction" by Quine; it is also (more commonly) called a "class builder" in the literature. An alternate definition using no existential quantifiers is shown by dfopab2 7381. For example, 𝑅 = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ (𝑥 + 1) = 𝑦)} → 3𝑅4 (ex-opab 27592). (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 4856 | . 2 class {〈𝑥, 𝑦〉 ∣ 𝜑} |
5 | vz | . . . . . . . 8 setvar 𝑧 | |
6 | 5 | cv 1623 | . . . . . . 7 class 𝑧 |
7 | 2 | cv 1623 | . . . . . . . 8 class 𝑥 |
8 | 3 | cv 1623 | . . . . . . . 8 class 𝑦 |
9 | 7, 8 | cop 4319 | . . . . . . 7 class 〈𝑥, 𝑦〉 |
10 | 6, 9 | wceq 1624 | . . . . . 6 wff 𝑧 = 〈𝑥, 𝑦〉 |
11 | 10, 1 | wa 383 | . . . . 5 wff (𝑧 = 〈𝑥, 𝑦〉 ∧ 𝜑) |
12 | 11, 3 | wex 1845 | . . . 4 wff ∃𝑦(𝑧 = 〈𝑥, 𝑦〉 ∧ 𝜑) |
13 | 12, 2 | wex 1845 | . . 3 wff ∃𝑥∃𝑦(𝑧 = 〈𝑥, 𝑦〉 ∧ 𝜑) |
14 | 13, 5 | cab 2738 | . 2 class {𝑧 ∣ ∃𝑥∃𝑦(𝑧 = 〈𝑥, 𝑦〉 ∧ 𝜑)} |
15 | 4, 14 | wceq 1624 | 1 wff {〈𝑥, 𝑦〉 ∣ 𝜑} = {𝑧 ∣ ∃𝑥∃𝑦(𝑧 = 〈𝑥, 𝑦〉 ∧ 𝜑)} |
Colors of variables: wff setvar class |
This definition is referenced by: opabss 4858 opabbid 4859 nfopab 4862 nfopab1 4863 nfopab2 4864 cbvopab 4865 cbvopab1 4867 cbvopab2 4868 cbvopab1s 4869 cbvopab2v 4871 unopab 4872 opabid 5124 elopab 5125 ssopab2 5143 iunopab 5154 dfid3 5167 elxpi 5279 rabxp 5303 csbxp 5349 ssrel 5356 relopabi 5393 relopabiALT 5394 opabssxpd 5485 cnv0 5685 dfoprab2 6858 dmoprab 6898 dfopab2 7381 brdom7disj 9537 brdom6disj 9538 opabssi 29724 cnvoprabOLD 29799 cnfinltrel 33544 rnxrn 34471 dropab1 39145 dropab2 39146 csbxpgOLD 39545 csbxpgVD 39621 relopabVD 39628 |
Copyright terms: Public domain | W3C validator |