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

Definition df-oprab 6077
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 6076 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 6201. (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  set  x
3 vy . . 3  set  y
4 vz . . 3  set  z
51, 2, 3, 4coprab 6074 . 2  class  { <. <.
x ,  y >. ,  z >.  |  ph }
6 vw . . . . . . . . 9  set  w
76cv 1651 . . . . . . . 8  class  w
82cv 1651 . . . . . . . . . 10  class  x
93cv 1651 . . . . . . . . . 10  class  y
108, 9cop 3809 . . . . . . . . 9  class  <. x ,  y >.
114cv 1651 . . . . . . . . 9  class  z
1210, 11cop 3809 . . . . . . . 8  class  <. <. x ,  y >. ,  z
>.
137, 12wceq 1652 . . . . . . 7  wff  w  = 
<. <. x ,  y
>. ,  z >.
1413, 1wa 359 . . . . . 6  wff  ( w  =  <. <. x ,  y
>. ,  z >.  /\ 
ph )
1514, 4wex 1550 . . . . 5  wff  E. z
( w  =  <. <.
x ,  y >. ,  z >.  /\  ph )
1615, 3wex 1550 . . . 4  wff  E. y E. z ( w  = 
<. <. x ,  y
>. ,  z >.  /\ 
ph )
1716, 2wex 1550 . . 3  wff  E. x E. y E. z ( w  =  <. <. x ,  y >. ,  z
>.  /\  ph )
1817, 6cab 2421 . 2  class  { w  |  E. x E. y E. z ( w  = 
<. <. x ,  y
>. ,  z >.  /\ 
ph ) }
195, 18wceq 1652 1  wff  { <. <.
x ,  y >. ,  z >.  |  ph }  =  { w  |  E. x E. y E. z ( w  = 
<. <. x ,  y
>. ,  z >.  /\ 
ph ) }
Colors of variables: wff set class
This definition is referenced by:  oprabid  6097  dfoprab2  6113  nfoprab1  6115  nfoprab2  6116  nfoprab3  6117  nfoprab  6118  oprabbid  6119  ssoprab2  6122  cbvoprab2  6137  eloprabga  6152  oprabrexex2  6181  eloprabi  6405  mpt20  6419  dftpos3  6489  colinearex  25986
  Copyright terms: Public domain W3C validator