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

Definition df-oprab 5714
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 5713 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 5835. (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, 4copab2 5711 . 2  class  { <. <.
x ,  y >. ,  z >.  |  ph }
6 vw . . . . . . . . 9  set  w
76cv 1618 . . . . . . . 8  class  w
82cv 1618 . . . . . . . . . 10  class  x
93cv 1618 . . . . . . . . . 10  class  y
108, 9cop 3547 . . . . . . . . 9  class  <. x ,  y >.
114cv 1618 . . . . . . . . 9  class  z
1210, 11cop 3547 . . . . . . . 8  class  <. <. x ,  y >. ,  z
>.
137, 12wceq 1619 . . . . . . 7  wff  w  = 
<. <. x ,  y
>. ,  z >.
1413, 1wa 360 . . . . . 6  wff  ( w  =  <. <. x ,  y
>. ,  z >.  /\ 
ph )
1514, 4wex 1537 . . . . 5  wff  E. z
( w  =  <. <.
x ,  y >. ,  z >.  /\  ph )
1615, 3wex 1537 . . . 4  wff  E. y E. z ( w  = 
<. <. x ,  y
>. ,  z >.  /\ 
ph )
1716, 2wex 1537 . . 3  wff  E. x E. y E. z ( w  =  <. <. x ,  y >. ,  z
>.  /\  ph )
1817, 6cab 2239 . 2  class  { w  |  E. x E. y E. z ( w  = 
<. <. x ,  y
>. ,  z >.  /\ 
ph ) }
195, 18wceq 1619 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  5734  dfoprab2  5747  nfoprab1  5749  nfoprab2  5750  nfoprab3  5751  nfoprab  5752  oprabbid  5753  ssoprab2  5756  cbvoprab2  5771  eloprabga  5786  oprabrexex2  5815  eloprabi  6038  mpt20  6051  dftpos3  6104  colinearex  23857
  Copyright terms: Public domain W3C validator