![]() |
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 5315 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 7558. For example, 𝑅 = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ (𝑥 + 1) = 𝑦)} → 3𝑅4 (ex-opab 27989). (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 4991 | . 2 class {〈𝑥, 𝑦〉 ∣ 𝜑} |
5 | vz | . . . . . . . 8 setvar 𝑧 | |
6 | 5 | cv 1506 | . . . . . . 7 class 𝑧 |
7 | 2 | cv 1506 | . . . . . . . 8 class 𝑥 |
8 | 3 | cv 1506 | . . . . . . . 8 class 𝑦 |
9 | 7, 8 | cop 4447 | . . . . . . 7 class 〈𝑥, 𝑦〉 |
10 | 6, 9 | wceq 1507 | . . . . . 6 wff 𝑧 = 〈𝑥, 𝑦〉 |
11 | 10, 1 | wa 387 | . . . . 5 wff (𝑧 = 〈𝑥, 𝑦〉 ∧ 𝜑) |
12 | 11, 3 | wex 1742 | . . . 4 wff ∃𝑦(𝑧 = 〈𝑥, 𝑦〉 ∧ 𝜑) |
13 | 12, 2 | wex 1742 | . . 3 wff ∃𝑥∃𝑦(𝑧 = 〈𝑥, 𝑦〉 ∧ 𝜑) |
14 | 13, 5 | cab 2759 | . 2 class {𝑧 ∣ ∃𝑥∃𝑦(𝑧 = 〈𝑥, 𝑦〉 ∧ 𝜑)} |
15 | 4, 14 | wceq 1507 | 1 wff {〈𝑥, 𝑦〉 ∣ 𝜑} = {𝑧 ∣ ∃𝑥∃𝑦(𝑧 = 〈𝑥, 𝑦〉 ∧ 𝜑)} |
Colors of variables: wff setvar class |
This definition is referenced by: opabss 4993 opabbid 4994 nfopab 4997 nfopab1 4998 nfopab2 4999 cbvopab 5000 cbvopab1 5002 cbvopab2 5003 cbvopab1s 5004 cbvopab2v 5006 unopab 5007 opabid 5268 elopab 5269 ssopab2 5287 iunopab 5298 dfid3 5313 elxpi 5429 rabxp 5452 csbxp 5500 ssrel 5507 relopabi 5544 relopabiALT 5545 opabssxpd 5636 cnv0 5839 dfoprab2 7031 dmoprab 7071 dfopab2 7558 brdom7disj 9751 brdom6disj 9752 opabssi 30128 cnvoprabOLD 30208 rnxrn 35088 dropab1 40195 dropab2 40196 csbxpgVD 40644 relopabVD 40651 |
Copyright terms: Public domain | W3C validator |