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

Definition df-ov 5745
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 5775 and ovprc2 5776. 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 5746. (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 5742 . 2  class  ( A F B )
51, 2cop 3500 . . 3  class  <. A ,  B >.
65, 3cfv 5093 . 2  class  ( F `
 <. A ,  B >. )
74, 6wceq 1316 1  wff  ( A F B )  =  ( F `  <. A ,  B >. )
Colors of variables: wff set class
This definition is referenced by:  oveq  5748  oveq1  5749  oveq2  5750  nfovd  5768  fnovex  5772  ovexg  5773  ovprc  5774  fnotovb  5782  ffnov  5843  eqfnov  5845  fnovim  5847  ovid  5855  ovidig  5856  ov  5858  ovigg  5859  ov6g  5876  ovg  5877  ovres  5878  fovrn  5881  fnrnov  5884  foov  5885  fnovrn  5886  funimassov  5888  ovelimab  5889  ovconst2  5890  elmpocl  5936  oprssdmm  6037  mpofvex  6069  oprab2co  6083  algrflem  6094  algrflemg  6095  mpoxopn0yelv  6104  ovtposg  6124  addpiord  7092  mulpiord  7093  addvalex  7620  cnref1o  9408  ioof  9722  frecuzrdgrrn  10149  frec2uzrdg  10150  frecuzrdgrcl  10151  frecuzrdgsuc  10155  frecuzrdgrclt  10156  frecuzrdgg  10157  frecuzrdgsuctlem  10164  seq3val  10199  seqvalcd  10200  cnrecnv  10650  eucalgval  11662  eucalginv  11664  eucalglt  11665  eucalg  11667  sqpweven  11780  2sqpwodd  11781  isstructim  11900  isstructr  11901  txdis1cn  12374  lmcn2  12376  cnmpt12f  12382  cnmpt21  12387  cnmpt2t  12389  cnmpt22  12390  psmetxrge0  12428  xmeterval  12531  comet  12595  txmetcnp  12614  qtopbasss  12617  cnmetdval  12625  remetdval  12635  tgqioo  12643
  Copyright terms: Public domain W3C validator