# 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 the most common operation class builder is given by ovmpo . (Contributed by NM, 12-Mar-1995)

Ref Expression
Assertion df-oprab ${⊢}\left\{⟨⟨{x},{y}⟩,{z}⟩|{\phi }\right\}=\left\{{w}|\exists {x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\exists {z}\phantom{\rule{.4em}{0ex}}\left({w}=⟨⟨{x},{y}⟩,{z}⟩\wedge {\phi }\right)\right\}$

### Detailed syntax breakdown

Step Hyp Ref Expression
0 vx ${setvar}{x}$
1 vy ${setvar}{y}$
2 vz ${setvar}{z}$
3 wph ${wff}{\phi }$
4 3 0 1 2 coprab ${class}\left\{⟨⟨{x},{y}⟩,{z}⟩|{\phi }\right\}$
5 vw ${setvar}{w}$
6 5 cv ${setvar}{w}$
7 0 cv ${setvar}{x}$
8 1 cv ${setvar}{y}$
9 7 8 cop ${class}⟨{x},{y}⟩$
10 2 cv ${setvar}{z}$
11 9 10 cop ${class}⟨⟨{x},{y}⟩,{z}⟩$
12 6 11 wceq ${wff}{w}=⟨⟨{x},{y}⟩,{z}⟩$
13 12 3 wa ${wff}\left({w}=⟨⟨{x},{y}⟩,{z}⟩\wedge {\phi }\right)$
14 13 2 wex ${wff}\exists {z}\phantom{\rule{.4em}{0ex}}\left({w}=⟨⟨{x},{y}⟩,{z}⟩\wedge {\phi }\right)$
15 14 1 wex ${wff}\exists {y}\phantom{\rule{.4em}{0ex}}\exists {z}\phantom{\rule{.4em}{0ex}}\left({w}=⟨⟨{x},{y}⟩,{z}⟩\wedge {\phi }\right)$
16 15 0 wex ${wff}\exists {x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\exists {z}\phantom{\rule{.4em}{0ex}}\left({w}=⟨⟨{x},{y}⟩,{z}⟩\wedge {\phi }\right)$
17 16 5 cab ${class}\left\{{w}|\exists {x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\exists {z}\phantom{\rule{.4em}{0ex}}\left({w}=⟨⟨{x},{y}⟩,{z}⟩\wedge {\phi }\right)\right\}$
18 4 17 wceq ${wff}\left\{⟨⟨{x},{y}⟩,{z}⟩|{\phi }\right\}=\left\{{w}|\exists {x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\exists {z}\phantom{\rule{.4em}{0ex}}\left({w}=⟨⟨{x},{y}⟩,{z}⟩\wedge {\phi }\right)\right\}$