![]() |
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 5574 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 8058. An example is given by ex-opab 30362. (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 5207 | . 2 class {〈𝑥, 𝑦〉 ∣ 𝜑} |
5 | vz | . . . . . . . 8 setvar 𝑧 | |
6 | 5 | cv 1533 | . . . . . . 7 class 𝑧 |
7 | 2 | cv 1533 | . . . . . . . 8 class 𝑥 |
8 | 3 | cv 1533 | . . . . . . . 8 class 𝑦 |
9 | 7, 8 | cop 4629 | . . . . . . 7 class 〈𝑥, 𝑦〉 |
10 | 6, 9 | wceq 1534 | . . . . . 6 wff 𝑧 = 〈𝑥, 𝑦〉 |
11 | 10, 1 | wa 394 | . . . . 5 wff (𝑧 = 〈𝑥, 𝑦〉 ∧ 𝜑) |
12 | 11, 3 | wex 1774 | . . . 4 wff ∃𝑦(𝑧 = 〈𝑥, 𝑦〉 ∧ 𝜑) |
13 | 12, 2 | wex 1774 | . . 3 wff ∃𝑥∃𝑦(𝑧 = 〈𝑥, 𝑦〉 ∧ 𝜑) |
14 | 13, 5 | cab 2703 | . 2 class {𝑧 ∣ ∃𝑥∃𝑦(𝑧 = 〈𝑥, 𝑦〉 ∧ 𝜑)} |
15 | 4, 14 | wceq 1534 | 1 wff {〈𝑥, 𝑦〉 ∣ 𝜑} = {𝑧 ∣ ∃𝑥∃𝑦(𝑧 = 〈𝑥, 𝑦〉 ∧ 𝜑)} |
Colors of variables: wff setvar class |
This definition is referenced by: opabss 5209 opabbid 5210 opabbidv 5211 nfopabd 5213 nfopab1 5215 nfopab2 5216 cbvopab 5217 cbvopabv 5218 cbvopab1 5220 cbvopab1g 5221 cbvopab2 5222 cbvopab1s 5223 cbvopab1v 5224 cbvopab2v 5226 unopab 5227 opabidw 5522 opabid 5523 elopabw 5524 ssopab2 5544 iunopab 5557 iunopabOLD 5558 dfid2 5574 dfid3 5575 elxpi 5696 opabssxpd 5721 rabxp 5722 csbxp 5773 ssrelOLD 5781 relopabi 5820 relopabiALT 5821 cnv0 6144 dfoprab2 7475 dmoprab 7519 dfopab2 8058 brdom7disj 10565 brdom6disj 10566 opabssi 32533 cnvoprabOLD 32634 bj-dfid2ALT 36785 rnxrn 38109 dropab1 44158 dropab2 44159 csbxpgVD 44607 relopabVD 44614 |
Copyright terms: Public domain | W3C validator |