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

Definition df-ov 5824
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 (see 3p2e5 9852). 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 5849 and ovprc2 5850. On the other hand, we often find uses for this definition when  F is a proper class, such as  +o in oav 6507.  F is normally equal to a class of nested ordered pairs of the form defined by df-oprab 5825. (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 5821 . 2  class  ( A F B )
51, 2cop 3646 . . 3  class  <. A ,  B >.
65, 3cfv 5223 . 2  class  ( F `
 <. A ,  B >. )
74, 6wceq 1625 1  wff  ( A F B )  =  ( F `  <. A ,  B >. )
Colors of variables: wff set class
This definition is referenced by:  oveq  5827  oveq1  5828  oveq2  5829  nfovd  5843  ovex  5846  ovssunirn  5847  ovprc  5848  fnotovb  5857  ffnov  5911  eqfnov  5913  fnov  5915  ovid  5927  ovidig  5928  ov  5930  ovigg  5931  ov6g  5948  ovg  5949  ovres  5950  fovrn  5953  fnrnov  5956  foov  5957  fnovrn  5958  funimassov  5960  ovelimab  5961  ovconst2  5962  oprssdm  5965  ndmovg  5966  elmpt2cl  6024  1st2val  6108  2nd2val  6109  ovmptss  6163  oprab2co  6167  curry1  6173  curry2  6176  algrflem  6187  ovtpos  6212  seqomlem1  6459  seqomlem4  6462  brwitnlem  6503  cantnfvalf  7363  fseqenlem1  7648  axdc4lem  8078  fpwwe  8265  canthwelem  8269  addpiord  8505  mulpiord  8506  addpqnq  8559  mulpqnq  8562  recmulnq  8585  dmrecnq  8589  cnref1o  10346  ixxssxr  10664  om2uzrdg  11015  uzrdgsuci  11019  swrd00  11447  cnrecnv  11646  sadcf  12640  smupf  12665  eucalgval  12748  eucalginv  12750  eucalglt  12751  eucalg  12753  vdwmc  13021  isstruct2  13153  isstruct  13154  prdsval  13351  prdsplusg  13354  prdsmulr  13355  prdsvsca  13356  prdshom  13362  imasaddvallem  13427  imasvscafn  13435  imasvscaval  13436  xpsff1o  13466  xpsaddlem  13473  xpsvsca  13477  xpsle  13479  comffval  13598  comfffval2  13600  comfeq  13605  isoval  13663  isssc  13693  isfuncd  13735  funcf2  13738  idfu2nd  13747  idfucl  13751  cofucl  13758  resfval2  13763  resf2nd  13765  funcres2b  13767  funcpropd  13770  homarcl  13856  homaval  13859  homarcl2  13863  arwhoma  13873  coapm  13899  catcco  13929  catcisolem  13934  xpcco  13953  xpcid  13959  xpcpropd  13978  evlfcllem  13991  evlfcl  13992  curf1cl  13998  curf2cl  14001  curfcl  14002  uncf1  14006  uncf2  14007  uncfcurf  14009  diag11  14013  diag12  14014  diag2  14015  curf2ndf  14017  hof2fval  14025  hofcl  14029  hofpropd  14037  yonedalem21  14043  yonedalem22  14048  yonedalem3b  14049  yonedalem3  14050  yonedainv  14051  yonffthlem  14052  plusffval  14375  gaid  14749  oppglsm  14949  efgmnvl  15019  efgval2  15029  vrgpinv  15074  frgpuptinv  15076  frgpuplem  15077  frgpup2  15081  frgpup3lem  15082  frgpnabllem1  15157  gsum2d  15219  gsum2d2lem  15220  gsumcom2  15222  eldprd  15235  dprd2dlem2  15271  dprd2dlem1  15272  dprd2da  15273  scaffval  15641  ipffval  16548  iccordt  16940  iscnp2  16965  ptbasfi  17272  txcnpi  17298  txdis1cn  17325  lmcn2  17339  xkococn  17350  cnmpt12f  17356  cnmpt21  17361  cnmpt2t  17363  cnmpt22  17364  cnmpt2k  17378  xkohmeo  17502  flfcnp2  17698  tmdcn2  17768  clssubg  17787  tgphaus  17795  divstgplem  17799  imasdsf1olem  17933  xpsdsval  17941  xmeterval  17974  comet  18055  txmetcnp  18089  nrmmetd  18093  nmfval  18107  isngp3  18116  ngpds  18121  tngnm  18163  qtopbaslem  18263  cnmetdval  18276  remetdval  18291  tgqioo  18302  bndth  18452  htpyco2  18473  phtpyco2  18484  caubl  18729  caublcls  18730  bcthlem1  18742  bcthlem2  18743  bcthlem4  18745  bcthlem5  18746  ovolfioo  18823  ovolficc  18824  ovolficcss  18825  ovolfsval  18826  ovolctb  18845  ovoliunlem2  18858  ovolicc2lem1  18872  ovolicc2lem5  18876  ovolfs2  18922  ioorinv  18927  uniiccdif  18929  uniioovol  18930  uniiccvol  18931  uniioombllem2a  18933  uniioombllem2  18934  uniioombllem3a  18935  uniioombllem3  18936  uniioombllem4  18937  uniioombllem5  18938  uniioombllem6  18939  dyadovol  18944  dyadss  18945  dyaddisjlem  18946  dyadmaxlem  18948  dyadmbl  18951  opnmbllem  18952  itg1addlem4  19050  limccnp2  19238  dvbsss  19248  perfdvf  19249  dvdsmulf1o  20430  fsumdvdsmul  20431  fsumvma  20448  grposn  20876  rngosn  21065  imsdval  21249  cvmlift2lem9  23248  cvmlift2lem10  23249  cvmlift2lem13  23252  cvmliftphtlem  23254  fvtransport  24064  fvray  24173  linedegen  24175  fvline  24176  oprssopvg  24434  fnovpop  24438  fnovrn2  24450  cbcpcp  24563  ltrcmp  24806  islimrs  24981  vecaddonto  25060  vecscmonto  25087  1ded  25139  1cat  25160  ishomb  25189  isfuna  25235  valtar  25284  cmpmor  25376  opropabco  25790  f1opr  25792  ismtyhmeolem  25929  heiborlem3  25938  heiborlem4  25939  heiborlem6  25941  heiborlem8  25943  mamudi  26862  mamudir  26863  mamuvs1  26864  mamuvs2  26865  matrcl  26867  aovfundmoveq  27422  aovpcov0  27431  aovnuoveq  27432  aovvoveq  27433  aov0ov0  27434  aovovn0oveq  27435  aov0nbovbi  27436  aovov0bi  27437  logb2aval  27522
  Copyright terms: Public domain W3C validator