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

Definition df-oprab 5459
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 , , and are distinct, although the definition doesn't strictly require it. See df-ov 5458 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 5578. (Contributed by NM, 12-Mar-1995.)
Assertion
Ref Expression
df-oprab  { <. <. ,  >. ,  >.  |  }  {  |  <. <. ,  >. ,  >.  }
Distinct variable groups:   ,   ,   ,   ,
Allowed substitution hints:   (,,)

Detailed syntax breakdown of Definition df-oprab
StepHypRef Expression
1 wph . . 3
2 vx . . 3  setvar
3 vy . . 3  setvar
4 vz . . 3  setvar
51, 2, 3, 4coprab 5456 . 2  { <. <. ,  >. ,  >.  |  }
6 vw . . . . . . . . 9  setvar
76cv 1241 . . . . . . . 8
82cv 1241 . . . . . . . . . 10
93cv 1241 . . . . . . . . . 10
108, 9cop 3370 . . . . . . . . 9  <. ,  >.
114cv 1241 . . . . . . . . 9
1210, 11cop 3370 . . . . . . . 8  <. <. ,  >. ,  >.
137, 12wceq 1242 . . . . . . 7  <. <. , 
>. ,  >.
1413, 1wa 97 . . . . . 6  <. <. ,  >. ,  >.
1514, 4wex 1378 . . . . 5  <. <. ,  >. ,  >.
1615, 3wex 1378 . . . 4 
<. <. , 
>. ,  >.
1716, 2wex 1378 . . 3  <. <. ,  >. ,  >.
1817, 6cab 2023 . 2  {  | 
<. <. , 
>. ,  >.  }
195, 18wceq 1242 1  { <. <. ,  >. ,  >.  |  }  {  |  <. <. ,  >. ,  >.  }
Colors of variables: wff set class
This definition is referenced by:  oprabid  5480  dfoprab2  5494  nfoprab1  5496  nfoprab2  5497  nfoprab3  5498  nfoprab  5499  oprabbid  5500  ssoprab2  5503  mpt20  5516  cbvoprab2  5519  eloprabga  5533  oprabrexex2  5699  eloprabi  5764  dftpos3  5818
  Copyright terms: Public domain W3C validator