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

Definition df-oprab 6200
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 6199 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 6337. (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 6197 . 2  class  { <. <.
x ,  y >. ,  z >.  |  ph }
6 vw . . . . . . . . 9  setvar  w
76cv 1398 . . . . . . . 8  class  w
82cv 1398 . . . . . . . . . 10  class  x
93cv 1398 . . . . . . . . . 10  class  y
108, 9cop 3950 . . . . . . . . 9  class  <. x ,  y >.
114cv 1398 . . . . . . . . 9  class  z
1210, 11cop 3950 . . . . . . . 8  class  <. <. x ,  y >. ,  z
>.
137, 12wceq 1399 . . . . . . 7  wff  w  = 
<. <. x ,  y
>. ,  z >.
1413, 1wa 367 . . . . . 6  wff  ( w  =  <. <. x ,  y
>. ,  z >.  /\ 
ph )
1514, 4wex 1620 . . . . 5  wff  E. z
( w  =  <. <.
x ,  y >. ,  z >.  /\  ph )
1615, 3wex 1620 . . . 4  wff  E. y E. z ( w  = 
<. <. x ,  y
>. ,  z >.  /\ 
ph )
1716, 2wex 1620 . . 3  wff  E. x E. y E. z ( w  =  <. <. x ,  y >. ,  z
>.  /\  ph )
1817, 6cab 2367 . 2  class  { w  |  E. x E. y E. z ( w  = 
<. <. x ,  y
>. ,  z >.  /\ 
ph ) }
195, 18wceq 1399 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  6223  dfoprab2  6242  nfoprab1  6245  nfoprab2  6246  nfoprab3  6247  nfoprab  6248  oprabbid  6249  ssoprab2  6252  mpt20  6266  cbvoprab2  6269  eloprabga  6288  oprabrexex2  6689  eloprabi  6761  dftpos3  6891  meet0  15884  join0  15885  cnvoprab  27696  mppspstlem  29120  mppsval  29121  colinearex  29863
  Copyright terms: Public domain W3C validator