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

Definition df-ov 5713
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 9734). 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 5738 and ovprc2 5739. On the other hand, we often find uses for this definition when  F is a proper class, such as  +o in oav 6396.  F is normally equal to a class of nested ordered pairs of the form defined by df-oprab 5714. (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 5710 . 2  class  ( A F B )
51, 2cop 3547 . . 3  class  <. A ,  B >.
65, 3cfv 4592 . 2  class  ( F `
 <. A ,  B >. )
74, 6wceq 1619 1  wff  ( A F B )  =  ( F `  <. A ,  B >. )
Colors of variables: wff set class
This definition is referenced by:  oveq  5716  oveq1  5717  oveq2  5718  nfovd  5732  ovex  5735  ovssunirn  5736  ovprc  5737  fnotovb  5746  ffnov  5800  eqfnov  5802  fnov  5804  ovid  5816  ovidig  5817  ov  5819  ovigg  5820  ov6g  5837  ovg  5838  ovres  5839  fovrn  5842  fnrnov  5845  foov  5846  fnovrn  5847  funimassov  5849  ovelimab  5850  ovconst2  5851  oprssdm  5854  ndmovg  5855  elmpt2cl  5913  1st2val  5997  2nd2val  5998  ovmptss  6052  oprab2co  6056  curry1  6062  curry2  6065  algrflem  6076  ovtpos  6101  seqomlem1  6348  seqomlem4  6351  brwitnlem  6392  cantnfvalf  7250  fseqenlem1  7535  axdc4lem  7965  fpwwe  8148  canthwelem  8152  addpiord  8388  mulpiord  8389  addpqnq  8442  mulpqnq  8445  recmulnq  8468  dmrecnq  8472  cnref1o  10228  ixxssxr  10546  om2uzrdg  10897  uzrdgsuci  10901  swrd00  11328  cnrecnv  11527  sadcf  12518  smupf  12543  eucalgval  12626  eucalginv  12628  eucalglt  12629  eucalg  12631  vdwmc  12899  isstruct2  13031  isstruct  13032  prdsval  13229  prdsplusg  13232  prdsmulr  13233  prdsvsca  13234  prdshom  13240  imasaddvallem  13305  imasvscafn  13313  imasvscaval  13314  xpsff1o  13344  xpsaddlem  13351  xpsvsca  13355  xpsle  13357  comffval  13446  comfffval2  13448  comfeq  13453  isoval  13511  isssc  13541  isfuncd  13583  funcf2  13586  idfu2nd  13595  idfucl  13599  cofucl  13606  resfval2  13611  resf2nd  13613  funcres2b  13615  funcpropd  13618  homarcl  13704  homaval  13707  homarcl2  13711  arwhoma  13721  coapm  13747  catcco  13777  catcisolem  13782  xpcco  13801  xpcid  13807  xpcpropd  13826  evlfcllem  13839  evlfcl  13840  curf1cl  13846  curf2cl  13849  curfcl  13850  uncf1  13854  uncf2  13855  uncfcurf  13857  diag11  13861  diag12  13862  diag2  13863  curf2ndf  13865  hof2fval  13873  hofcl  13877  hofpropd  13885  yonedalem21  13891  yonedalem22  13896  yonedalem3b  13897  yonedalem3  13898  yonedainv  13899  yonffthlem  13900  plusffval  14214  gaid  14588  oppglsm  14788  efgmnvl  14858  efgval2  14868  vrgpinv  14913  frgpuptinv  14915  frgpuplem  14916  frgpup2  14920  frgpup3lem  14921  frgpnabllem1  14996  gsum2d  15058  gsum2d2lem  15059  gsumcom2  15061  eldprd  15074  dprd2dlem2  15110  dprd2dlem1  15111  dprd2da  15112  scaffval  15480  ipffval  16384  iccordt  16776  iscnp2  16801  ptbasfi  17108  txcnpi  17134  txdis1cn  17161  lmcn2  17175  xkococn  17186  cnmpt12f  17192  cnmpt21  17197  cnmpt2t  17199  cnmpt22  17200  cnmpt2k  17214  xkohmeo  17338  flfcnp2  17534  tmdcn2  17604  clssubg  17623  tgphaus  17631  divstgplem  17635  imasdsf1olem  17769  xpsdsval  17777  xmeterval  17810  comet  17891  txmetcnp  17925  nrmmetd  17929  nmfval  17943  isngp3  17952  ngpds  17957  tngnm  17999  qtopbaslem  18099  cnmetdval  18112  remetdval  18127  tgqioo  18138  bndth  18288  htpyco2  18309  phtpyco2  18320  caubl  18565  caublcls  18566  bcthlem1  18578  bcthlem2  18579  bcthlem4  18581  bcthlem5  18582  ovolfioo  18659  ovolficc  18660  ovolficcss  18661  ovolfsval  18662  ovolctb  18681  ovoliunlem2  18694  ovolicc2lem1  18708  ovolicc2lem5  18712  ovolfs2  18758  ioorinv  18763  uniiccdif  18765  uniioovol  18766  uniiccvol  18767  uniioombllem2a  18769  uniioombllem2  18770  uniioombllem3a  18771  uniioombllem3  18772  uniioombllem4  18773  uniioombllem5  18774  uniioombllem6  18775  dyadovol  18780  dyadss  18781  dyaddisjlem  18782  dyadmaxlem  18784  dyadmbl  18787  opnmbllem  18788  itg1addlem4  18886  limccnp2  19074  dvbsss  19084  perfdvf  19085  dvdsmulf1o  20266  fsumdvdsmul  20267  fsumvma  20284  grposn  20712  rngosn  20901  imsdval  21085  cvmlift2lem9  23013  cvmlift2lem10  23014  cvmlift2lem13  23017  cvmliftphtlem  23019  fvtransport  23829  fvray  23938  linedegen  23940  fvline  23941  oprssopvg  24199  fnovpop  24203  fnovrn2  24215  cbcpcp  24328  ltrcmp  24571  islimrs  24746  vecaddonto  24825  vecscmonto  24852  1ded  24904  1cat  24925  ishomb  24954  isfuna  25000  valtar  25049  cmpmor  25141  opropabco  25555  f1opr  25557  ismtyhmeolem  25694  heiborlem3  25703  heiborlem4  25704  heiborlem6  25706  heiborlem8  25708  mamudi  26627  mamudir  26628  mamuvs1  26629  mamuvs2  26630  matrcl  26632  logbval  26949
  Copyright terms: Public domain W3C validator