Metamath Proof Explorer


Definition df-oprab

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 { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 } = { 𝑤 ∣ ∃ 𝑥𝑦𝑧 ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜑 ) }

Detailed syntax breakdown

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 { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 } = { 𝑤 ∣ ∃ 𝑥𝑦𝑧 ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜑 ) }