![]() |
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 5056 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 7266. For example, 𝑅 = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ (𝑥 + 1) = 𝑦)} → 3𝑅4 (ex-opab 27419). (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 4745 | . 2 class {〈𝑥, 𝑦〉 ∣ 𝜑} |
5 | vz | . . . . . . . 8 setvar 𝑧 | |
6 | 5 | cv 1522 | . . . . . . 7 class 𝑧 |
7 | 2 | cv 1522 | . . . . . . . 8 class 𝑥 |
8 | 3 | cv 1522 | . . . . . . . 8 class 𝑦 |
9 | 7, 8 | cop 4216 | . . . . . . 7 class 〈𝑥, 𝑦〉 |
10 | 6, 9 | wceq 1523 | . . . . . 6 wff 𝑧 = 〈𝑥, 𝑦〉 |
11 | 10, 1 | wa 383 | . . . . 5 wff (𝑧 = 〈𝑥, 𝑦〉 ∧ 𝜑) |
12 | 11, 3 | wex 1744 | . . . 4 wff ∃𝑦(𝑧 = 〈𝑥, 𝑦〉 ∧ 𝜑) |
13 | 12, 2 | wex 1744 | . . 3 wff ∃𝑥∃𝑦(𝑧 = 〈𝑥, 𝑦〉 ∧ 𝜑) |
14 | 13, 5 | cab 2637 | . 2 class {𝑧 ∣ ∃𝑥∃𝑦(𝑧 = 〈𝑥, 𝑦〉 ∧ 𝜑)} |
15 | 4, 14 | wceq 1523 | 1 wff {〈𝑥, 𝑦〉 ∣ 𝜑} = {𝑧 ∣ ∃𝑥∃𝑦(𝑧 = 〈𝑥, 𝑦〉 ∧ 𝜑)} |
Colors of variables: wff setvar class |
This definition is referenced by: opabss 4747 opabbid 4748 nfopab 4751 nfopab1 4752 nfopab2 4753 cbvopab 4754 cbvopab1 4756 cbvopab2 4757 cbvopab1s 4758 cbvopab2v 4760 unopab 4761 opabid 5011 elopab 5012 ssopab2 5030 iunopab 5041 dfid3 5054 elxpi 5164 rabxp 5188 csbxp 5234 ssrel 5241 relopabi 5278 relopabiALT 5279 opabssxpd 5370 cnv0 5570 dfoprab2 6743 dmoprab 6783 dfopab2 7266 brdom7disj 9391 brdom6disj 9392 opabssi 29551 cnvoprabOLD 29626 rnxrn 34296 dropab1 38968 dropab2 38969 csbxpgOLD 39368 csbxpgVD 39444 relopabVD 39451 |
Copyright terms: Public domain | W3C validator |