Description: Define the class abstraction (class builder) of a collection of nested ordered pairs (for use in defining operations). This is a special case of Definition 4.16 of TakeutiZaring p. 14. Normally x , y , and z are distinct, although the definition doesn't strictly require it. See df-ov for the value of an operation. The brace notation is called "class abstraction" by Quine; it is also called a "class builder" in the literature. The value of an operation given by a class abstraction is given by ovmpo . (Contributed by NM, 12-Mar-1995)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | df-oprab | ⊢ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 } = { 𝑤 ∣ ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜑 ) } |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | vx | ⊢ 𝑥 | |
| 1 | vy | ⊢ 𝑦 | |
| 2 | vz | ⊢ 𝑧 | |
| 3 | wph | ⊢ 𝜑 | |
| 4 | 3 0 1 2 | coprab | ⊢ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 } |
| 5 | vw | ⊢ 𝑤 | |
| 6 | 5 | cv | ⊢ 𝑤 |
| 7 | 0 | cv | ⊢ 𝑥 |
| 8 | 1 | cv | ⊢ 𝑦 |
| 9 | 7 8 | cop | ⊢ ⟨ 𝑥 , 𝑦 ⟩ |
| 10 | 2 | cv | ⊢ 𝑧 |
| 11 | 9 10 | cop | ⊢ ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ |
| 12 | 6 11 | wceq | ⊢ 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ |
| 13 | 12 3 | wa | ⊢ ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜑 ) |
| 14 | 13 2 | wex | ⊢ ∃ 𝑧 ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜑 ) |
| 15 | 14 1 | wex | ⊢ ∃ 𝑦 ∃ 𝑧 ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜑 ) |
| 16 | 15 0 | wex | ⊢ ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜑 ) |
| 17 | 16 5 | cab | ⊢ { 𝑤 ∣ ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜑 ) } |
| 18 | 4 17 | wceq | ⊢ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 } = { 𝑤 ∣ ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜑 ) } |