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 5457 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 7741. An example is given by ex-opab 28139. (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 5120 | . 2 class {〈𝑥, 𝑦〉 ∣ 𝜑} |
5 | vz | . . . . . . . 8 setvar 𝑧 | |
6 | 5 | cv 1527 | . . . . . . 7 class 𝑧 |
7 | 2 | cv 1527 | . . . . . . . 8 class 𝑥 |
8 | 3 | cv 1527 | . . . . . . . 8 class 𝑦 |
9 | 7, 8 | cop 4565 | . . . . . . 7 class 〈𝑥, 𝑦〉 |
10 | 6, 9 | wceq 1528 | . . . . . 6 wff 𝑧 = 〈𝑥, 𝑦〉 |
11 | 10, 1 | wa 396 | . . . . 5 wff (𝑧 = 〈𝑥, 𝑦〉 ∧ 𝜑) |
12 | 11, 3 | wex 1771 | . . . 4 wff ∃𝑦(𝑧 = 〈𝑥, 𝑦〉 ∧ 𝜑) |
13 | 12, 2 | wex 1771 | . . 3 wff ∃𝑥∃𝑦(𝑧 = 〈𝑥, 𝑦〉 ∧ 𝜑) |
14 | 13, 5 | cab 2799 | . 2 class {𝑧 ∣ ∃𝑥∃𝑦(𝑧 = 〈𝑥, 𝑦〉 ∧ 𝜑)} |
15 | 4, 14 | wceq 1528 | 1 wff {〈𝑥, 𝑦〉 ∣ 𝜑} = {𝑧 ∣ ∃𝑥∃𝑦(𝑧 = 〈𝑥, 𝑦〉 ∧ 𝜑)} |
Colors of variables: wff setvar class |
This definition is referenced by: opabss 5122 opabbid 5123 nfopab 5126 nfopab1 5127 nfopab2 5128 cbvopab 5129 cbvopab1 5131 cbvopab1g 5132 cbvopab2 5133 cbvopab1s 5134 cbvopab2v 5136 unopab 5137 opabidw 5404 opabid 5405 elopab 5406 ssopab2 5425 iunopab 5438 dfid3 5456 elxpi 5571 rabxp 5594 csbxp 5644 ssrel 5651 relopabi 5688 relopabiALT 5689 opabssxpd 5783 cnv0 5993 dfoprab2 7201 dmoprab 7244 dfopab2 7741 brdom7disj 9942 brdom6disj 9943 opabssi 30293 cnvoprabOLD 30383 rnxrn 35528 dropab1 40659 dropab2 40660 csbxpgVD 41108 relopabVD 41115 |
Copyright terms: Public domain | W3C validator |