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

Definition df-oprab 6309
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 6308 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 6446. (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 6306 . 2  class  { <. <.
x ,  y >. ,  z >.  |  ph }
6 vw . . . . . . . . 9  setvar  w
76cv 1436 . . . . . . . 8  class  w
82cv 1436 . . . . . . . . . 10  class  x
93cv 1436 . . . . . . . . . 10  class  y
108, 9cop 4008 . . . . . . . . 9  class  <. x ,  y >.
114cv 1436 . . . . . . . . 9  class  z
1210, 11cop 4008 . . . . . . . 8  class  <. <. x ,  y >. ,  z
>.
137, 12wceq 1437 . . . . . . 7  wff  w  = 
<. <. x ,  y
>. ,  z >.
1413, 1wa 370 . . . . . 6  wff  ( w  =  <. <. x ,  y
>. ,  z >.  /\ 
ph )
1514, 4wex 1659 . . . . 5  wff  E. z
( w  =  <. <.
x ,  y >. ,  z >.  /\  ph )
1615, 3wex 1659 . . . 4  wff  E. y E. z ( w  = 
<. <. x ,  y
>. ,  z >.  /\ 
ph )
1716, 2wex 1659 . . 3  wff  E. x E. y E. z ( w  =  <. <. x ,  y >. ,  z
>.  /\  ph )
1817, 6cab 2414 . 2  class  { w  |  E. x E. y E. z ( w  = 
<. <. x ,  y
>. ,  z >.  /\ 
ph ) }
195, 18wceq 1437 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  6332  dfoprab2  6351  nfoprab1  6354  nfoprab2  6355  nfoprab3  6356  nfoprab  6357  oprabbid  6358  ssoprab2  6361  mpt20  6375  cbvoprab2  6378  eloprabga  6397  oprabrexex2  6797  eloprabi  6869  dftpos3  6999  meet0  16334  join0  16335  cnvoprab  28151  mppspstlem  29997  mppsval  29998  colinearex  30612
  Copyright terms: Public domain W3C validator