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

Definition df-ov 5566
Description: Define the value of an operation. Definition of operation value in [Enderton] p. 79. Note that the syntax is simply three class expressions in a row bracketed by parentheses. There are no restrictions of any kind on what those class expressions may be, although only certain kinds of class expressions - a binary operation  F and its arguments  A and  B- will be useful for proving meaningful theorems. For example, if class  F is the operation + and arguments  A and  B are 3 and 2 , the expression ( 3 + 2 ) can be proved to equal 5 . This definition is well-defined, although not very meaningful, when classes  A and/or  B are proper classes (i.e. are not sets); see ovprc1 5592 and ovprc2 5593. On the other hand, we often find uses for this definition when  F is a proper class.  F is normally equal to a class of nested ordered pairs of the form defined by df-oprab 5567. (Contributed by NM, 28-Feb-1995.)
Assertion
Ref Expression
df-ov  |-  ( A F B )  =  ( F `  <. A ,  B >. )

Detailed syntax breakdown of Definition df-ov
StepHypRef Expression
1 cA . . 3  class  A
2 cB . . 3  class  B
3 cF . . 3  class  F
41, 2, 3co 5563 . 2  class  ( A F B )
51, 2cop 3419 . . 3  class  <. A ,  B >.
65, 3cfv 4952 . 2  class  ( F `
 <. A ,  B >. )
74, 6wceq 1285 1  wff  ( A F B )  =  ( F `  <. A ,  B >. )
Colors of variables: wff set class
This definition is referenced by:  oveq  5569  oveq1  5570  oveq2  5571  nfovd  5585  fnovex  5589  ovexg  5590  ovprc  5591  fnotovb  5599  ffnov  5656  eqfnov  5658  fnovim  5660  ovid  5668  ovidig  5669  ov  5671  ovigg  5672  ov6g  5689  ovg  5690  ovres  5691  fovrn  5694  fnrnov  5697  foov  5698  fnovrn  5699  funimassov  5701  ovelimab  5702  ovconst2  5703  elmpt2cl  5749  mpt2fvex  5880  oprab2co  5890  algrflem  5901  algrflemg  5902  mpt2xopn0yelv  5908  ovtposg  5928  addpiord  6620  mulpiord  6621  addvalex  7126  cnref1o  8866  ioof  9122  frecuzrdgrrn  9542  frec2uzrdg  9543  frecuzrdgrcl  9544  frecuzrdgsuc  9548  frecuzrdgrclt  9549  frecuzrdgg  9550  frecuzrdgsuctlem  9557  iseqvalt  9584  cnrecnv  9998  eucalgval  10643  eucalginv  10645  eucalglt  10646  eucialg  10648  sqpweven  10760  2sqpwodd  10761
  Copyright terms: Public domain W3C validator