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

Definition df-ov 5861
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 9855). 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 5886 and ovprc2 5887. On the other hand, we often find uses for this definition when  F is a proper class, such as  +o in oav 6510.  F is normally equal to a class of nested ordered pairs of the form defined by df-oprab 5862. (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 5858 . 2  class  ( A F B )
51, 2cop 3643 . . 3  class  <. A ,  B >.
65, 3cfv 5255 . 2  class  ( F `
 <. A ,  B >. )
74, 6wceq 1623 1  wff  ( A F B )  =  ( F `  <. A ,  B >. )
Colors of variables: wff set class
This definition is referenced by:  oveq  5864  oveq1  5865  oveq2  5866  nfovd  5880  ovex  5883  ovssunirn  5884  ovprc  5885  fnotovb  5894  ffnov  5948  eqfnov  5950  fnov  5952  ovid  5964  ovidig  5965  ov  5967  ovigg  5968  ov6g  5985  ovg  5986  ovres  5987  fovrn  5990  fnrnov  5993  foov  5994  fnovrn  5995  funimassov  5997  ovelimab  5998  ovconst2  5999  oprssdm  6002  ndmovg  6003  elmpt2cl  6061  1st2val  6145  2nd2val  6146  ovmptss  6200  oprab2co  6204  curry1  6210  curry2  6213  algrflem  6224  ovtpos  6249  seqomlem1  6462  seqomlem4  6465  brwitnlem  6506  cantnfvalf  7366  fseqenlem1  7651  axdc4lem  8081  fpwwe  8268  canthwelem  8272  addpiord  8508  mulpiord  8509  addpqnq  8562  mulpqnq  8565  recmulnq  8588  dmrecnq  8592  cnref1o  10349  ixxssxr  10668  om2uzrdg  11019  uzrdgsuci  11023  swrd00  11451  cnrecnv  11650  sadcf  12644  smupf  12669  eucalgval  12752  eucalginv  12754  eucalglt  12755  eucalg  12757  vdwmc  13025  isstruct2  13157  isstruct  13158  prdsval  13355  prdsplusg  13358  prdsmulr  13359  prdsvsca  13360  prdshom  13366  imasaddvallem  13431  imasvscafn  13439  imasvscaval  13440  xpsff1o  13470  xpsaddlem  13477  xpsvsca  13481  xpsle  13483  comffval  13602  comfffval2  13604  comfeq  13609  isoval  13667  isssc  13697  isfuncd  13739  funcf2  13742  idfu2nd  13751  idfucl  13755  cofucl  13762  resfval2  13767  resf2nd  13769  funcres2b  13771  funcpropd  13774  homarcl  13860  homaval  13863  homarcl2  13867  arwhoma  13877  coapm  13903  catcco  13933  catcisolem  13938  xpcco  13957  xpcid  13963  xpcpropd  13982  evlfcllem  13995  evlfcl  13996  curf1cl  14002  curf2cl  14005  curfcl  14006  uncf1  14010  uncf2  14011  uncfcurf  14013  diag11  14017  diag12  14018  diag2  14019  curf2ndf  14021  hof2fval  14029  hofcl  14033  hofpropd  14041  yonedalem21  14047  yonedalem22  14052  yonedalem3b  14053  yonedalem3  14054  yonedainv  14055  yonffthlem  14056  plusffval  14379  gaid  14753  oppglsm  14953  efgmnvl  15023  efgval2  15033  vrgpinv  15078  frgpuptinv  15080  frgpuplem  15081  frgpup2  15085  frgpup3lem  15086  frgpnabllem1  15161  gsum2d  15223  gsum2d2lem  15224  gsumcom2  15226  eldprd  15239  dprd2dlem2  15275  dprd2dlem1  15276  dprd2da  15277  scaffval  15645  ipffval  16552  iccordt  16944  iscnp2  16969  ptbasfi  17276  txcnpi  17302  txdis1cn  17329  lmcn2  17343  xkococn  17354  cnmpt12f  17360  cnmpt21  17365  cnmpt2t  17367  cnmpt22  17368  cnmpt2k  17382  xkohmeo  17506  flfcnp2  17702  tmdcn2  17772  clssubg  17791  tgphaus  17799  divstgplem  17803  imasdsf1olem  17937  xpsdsval  17945  xmeterval  17978  comet  18059  txmetcnp  18093  nrmmetd  18097  nmfval  18111  isngp3  18120  ngpds  18125  tngnm  18167  qtopbaslem  18267  cnmetdval  18280  remetdval  18295  tgqioo  18306  bndth  18456  htpyco2  18477  phtpyco2  18488  caubl  18733  caublcls  18734  bcthlem1  18746  bcthlem2  18747  bcthlem4  18749  bcthlem5  18750  ovolfioo  18827  ovolficc  18828  ovolficcss  18829  ovolfsval  18830  ovolctb  18849  ovoliunlem2  18862  ovolicc2lem1  18876  ovolicc2lem5  18880  ovolfs2  18926  ioorinv  18931  uniiccdif  18933  uniioovol  18934  uniiccvol  18935  uniioombllem2a  18937  uniioombllem2  18938  uniioombllem3a  18939  uniioombllem3  18940  uniioombllem4  18941  uniioombllem5  18942  uniioombllem6  18943  dyadovol  18948  dyadss  18949  dyaddisjlem  18950  dyadmaxlem  18952  dyadmbl  18955  opnmbllem  18956  itg1addlem4  19054  limccnp2  19242  dvbsss  19252  perfdvf  19253  dvdsmulf1o  20434  fsumdvdsmul  20435  fsumvma  20452  grposn  20882  rngosn  21071  imsdval  21255  elovimad  23205  ofoprabco  23232  xrofsup  23255  logb2aval  23393  ismbfm  23557  cndprobval  23636  cvmlift2lem9  23842  cvmlift2lem10  23843  cvmlift2lem13  23846  cvmliftphtlem  23848  fvtransport  24655  fvray  24764  linedegen  24766  fvline  24767  oprssopvg  25034  fnovpop  25038  fnovrn2  25050  cbcpcp  25162  ltrcmp  25405  islimrs  25580  vecaddonto  25659  vecscmonto  25686  1ded  25738  1cat  25759  ishomb  25788  isfuna  25834  valtar  25883  cmpmor  25975  opropabco  26389  f1opr  26391  ismtyhmeolem  26528  heiborlem3  26537  heiborlem4  26538  heiborlem6  26540  heiborlem8  26542  mamudi  27461  mamudir  27462  mamuvs1  27463  mamuvs2  27464  matrcl  27466  aovfundmoveq  28041  aovpcov0  28050  aovnuoveq  28051  aovvoveq  28052  aov0ov0  28053  aovovn0oveq  28054  aov0nbovbi  28055  aovov0bi  28056  nssdmovg  28077  mpt2xopn0yelv  28079  mpt2xopxnop0  28081  nbgrael  28141
  Copyright terms: Public domain W3C validator