MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-oprab Structured version   Visualization version   Unicode version

Definition df-oprab 6319
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 6318 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 ovmpt2 6459. (Contributed by NM, 12-Mar-1995.)
Assertion
Ref Expression
df-oprab  |-  { <. <.
x ,  y >. ,  z >.  |  ph }  =  { w  |  E. x E. y E. z ( w  = 
<. <. x ,  y
>. ,  z >.  /\ 
ph ) }
Distinct variable groups:    x, w    y, w    z, w    ph, w
Allowed substitution hints:    ph( x, y, z)

Detailed syntax breakdown of Definition df-oprab
StepHypRef Expression
1 wph . . 3  wff  ph
2 vx . . 3  setvar  x
3 vy . . 3  setvar  y
4 vz . . 3  setvar  z
51, 2, 3, 4coprab 6316 . 2  class  { <. <.
x ,  y >. ,  z >.  |  ph }
6 vw . . . . . . . . 9  setvar  w
76cv 1454 . . . . . . . 8  class  w
82cv 1454 . . . . . . . . . 10  class  x
93cv 1454 . . . . . . . . . 10  class  y
108, 9cop 3986 . . . . . . . . 9  class  <. x ,  y >.
114cv 1454 . . . . . . . . 9  class  z
1210, 11cop 3986 . . . . . . . 8  class  <. <. x ,  y >. ,  z
>.
137, 12wceq 1455 . . . . . . 7  wff  w  = 
<. <. x ,  y
>. ,  z >.
1413, 1wa 375 . . . . . 6  wff  ( w  =  <. <. x ,  y
>. ,  z >.  /\ 
ph )
1514, 4wex 1674 . . . . 5  wff  E. z
( w  =  <. <.
x ,  y >. ,  z >.  /\  ph )
1615, 3wex 1674 . . . 4  wff  E. y E. z ( w  = 
<. <. x ,  y
>. ,  z >.  /\ 
ph )
1716, 2wex 1674 . . 3  wff  E. x E. y E. z ( w  =  <. <. x ,  y >. ,  z
>.  /\  ph )
1817, 6cab 2448 . 2  class  { w  |  E. x E. y E. z ( w  = 
<. <. x ,  y
>. ,  z >.  /\ 
ph ) }
195, 18wceq 1455 1  wff  { <. <.
x ,  y >. ,  z >.  |  ph }  =  { w  |  E. x E. y E. z ( w  = 
<. <. x ,  y
>. ,  z >.  /\ 
ph ) }
Colors of variables: wff setvar class
This definition is referenced by:  oprabid  6342  dfoprab2  6364  nfoprab1  6367  nfoprab2  6368  nfoprab3  6369  nfoprab  6370  oprabbid  6371  ssoprab2  6374  mpt20  6388  cbvoprab2  6391  eloprabga  6410  oprabrexex2  6810  eloprabi  6882  dftpos3  7017  meet0  16432  join0  16433  cnvoprab  28357  mppspstlem  30258  mppsval  30259  colinearex  30876  csboprabg  31776
  Copyright terms: Public domain W3C validator