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 4956 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 7113. For example, 𝑅 = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ (𝑥 + 1) = 𝑦)} → 3𝑅4 (ex-opab 26681). (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 4642 | . 2 class {〈𝑥, 𝑦〉 ∣ 𝜑} |
5 | vz | . . . . . . . 8 setvar 𝑧 | |
6 | 5 | cv 1474 | . . . . . . 7 class 𝑧 |
7 | 2 | cv 1474 | . . . . . . . 8 class 𝑥 |
8 | 3 | cv 1474 | . . . . . . . 8 class 𝑦 |
9 | 7, 8 | cop 4131 | . . . . . . 7 class 〈𝑥, 𝑦〉 |
10 | 6, 9 | wceq 1475 | . . . . . 6 wff 𝑧 = 〈𝑥, 𝑦〉 |
11 | 10, 1 | wa 383 | . . . . 5 wff (𝑧 = 〈𝑥, 𝑦〉 ∧ 𝜑) |
12 | 11, 3 | wex 1695 | . . . 4 wff ∃𝑦(𝑧 = 〈𝑥, 𝑦〉 ∧ 𝜑) |
13 | 12, 2 | wex 1695 | . . 3 wff ∃𝑥∃𝑦(𝑧 = 〈𝑥, 𝑦〉 ∧ 𝜑) |
14 | 13, 5 | cab 2596 | . 2 class {𝑧 ∣ ∃𝑥∃𝑦(𝑧 = 〈𝑥, 𝑦〉 ∧ 𝜑)} |
15 | 4, 14 | wceq 1475 | 1 wff {〈𝑥, 𝑦〉 ∣ 𝜑} = {𝑧 ∣ ∃𝑥∃𝑦(𝑧 = 〈𝑥, 𝑦〉 ∧ 𝜑)} |
Colors of variables: wff setvar class |
This definition is referenced by: opabss 4646 opabbid 4647 nfopab 4650 nfopab1 4651 nfopab2 4652 cbvopab 4653 cbvopab1 4655 cbvopab2 4656 cbvopab1s 4657 cbvopab2v 4659 unopab 4660 opabid 4907 elopab 4908 ssopab2 4926 iunopab 4936 dfid3 4954 elxpi 5054 rabxp 5078 csbxp 5123 ssrel 5130 relopabi 5167 relopabiALT 5168 cnv0 5454 dfoprab2 6599 dmoprab 6639 opabex2 6997 dfopab2 7113 brdom7disj 9234 brdom6disj 9235 cnvoprab 28886 dropab1 37672 dropab2 37673 csbxpgOLD 38075 csbxpgVD 38152 relopabVD 38159 |
Copyright terms: Public domain | W3C validator |