ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-oprab Unicode version

Definition df-oprab 5881
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 5880 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 ovmpo 6012. (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 5878 . 2  class  { <. <.
x ,  y >. ,  z >.  |  ph }
6 vw . . . . . . . . 9  setvar  w
76cv 1352 . . . . . . . 8  class  w
82cv 1352 . . . . . . . . . 10  class  x
93cv 1352 . . . . . . . . . 10  class  y
108, 9cop 3597 . . . . . . . . 9  class  <. x ,  y >.
114cv 1352 . . . . . . . . 9  class  z
1210, 11cop 3597 . . . . . . . 8  class  <. <. x ,  y >. ,  z
>.
137, 12wceq 1353 . . . . . . 7  wff  w  = 
<. <. x ,  y
>. ,  z >.
1413, 1wa 104 . . . . . 6  wff  ( w  =  <. <. x ,  y
>. ,  z >.  /\ 
ph )
1514, 4wex 1492 . . . . 5  wff  E. z
( w  =  <. <.
x ,  y >. ,  z >.  /\  ph )
1615, 3wex 1492 . . . 4  wff  E. y E. z ( w  = 
<. <. x ,  y
>. ,  z >.  /\ 
ph )
1716, 2wex 1492 . . 3  wff  E. x E. y E. z ( w  =  <. <. x ,  y >. ,  z
>.  /\  ph )
1817, 6cab 2163 . 2  class  { w  |  E. x E. y E. z ( w  = 
<. <. x ,  y
>. ,  z >.  /\ 
ph ) }
195, 18wceq 1353 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  5909  dfoprab2  5924  nfoprab1  5926  nfoprab2  5927  nfoprab3  5928  nfoprab  5929  oprabbid  5930  ssoprab2  5933  mpo0  5947  cbvoprab2  5950  eloprabga  5964  oprabrexex2  6133  eloprabi  6199  cnvoprab  6237  dftpos3  6265
  Copyright terms: Public domain W3C validator