Description: Define the class abstraction of a collection of ordered pairs. Definition 3.3 of Monk1 p. 34. Usually x and y are distinct, although the definition does not require it (see dfid2 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 . An example is given by ex-opab . (Contributed by NM, 4-Jul-1994)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | df-opab | ⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } = { 𝑧 ∣ ∃ 𝑥 ∃ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) } |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | vx | ⊢ 𝑥 | |
| 1 | vy | ⊢ 𝑦 | |
| 2 | wph | ⊢ 𝜑 | |
| 3 | 2 0 1 | copab | ⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } |
| 4 | vz | ⊢ 𝑧 | |
| 5 | 4 | cv | ⊢ 𝑧 |
| 6 | 0 | cv | ⊢ 𝑥 |
| 7 | 1 | cv | ⊢ 𝑦 |
| 8 | 6 7 | cop | ⊢ ⟨ 𝑥 , 𝑦 ⟩ |
| 9 | 5 8 | wceq | ⊢ 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ |
| 10 | 9 2 | wa | ⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) |
| 11 | 10 1 | wex | ⊢ ∃ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) |
| 12 | 11 0 | wex | ⊢ ∃ 𝑥 ∃ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) |
| 13 | 12 4 | cab | ⊢ { 𝑧 ∣ ∃ 𝑥 ∃ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) } |
| 14 | 3 13 | wceq | ⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } = { 𝑧 ∣ ∃ 𝑥 ∃ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) } |