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

Definition df-ov 6279
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 10732). 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 6307 and ovprc2 6308. On the other hand, we often find uses for this definition when  F is a proper class, such as  +o in oav 7200.  F is normally equal to a class of nested ordered pairs of the form defined by df-oprab 6280. (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 6276 . 2  class  ( A F B )
51, 2cop 3942 . . 3  class  <. A ,  B >.
65, 3cfv 5561 . 2  class  ( F `
 <. A ,  B >. )
74, 6wceq 1448 1  wff  ( A F B )  =  ( F `  <. A ,  B >. )
Colors of variables: wff setvar class
This definition is referenced by:  oveq  6282  oveq1  6283  oveq2  6284  nfovd  6301  ovex  6304  ovssunirn  6305  ovprc  6306  csbov123  6310  csbov  6311  elovimad  6316  fnotovb  6317  ffnov  6388  eqfnov  6390  fnov  6392  ovid  6401  ovidig  6402  ov  6404  ovigg  6405  ov6g  6422  ovg  6423  ovres  6424  fovrn  6427  fnrnov  6430  foov  6431  fnovrn  6432  funimassov  6434  ovelimab  6435  ovima0  6436  ovconst2  6437  oprssdm  6438  nssdmovg  6439  ndmovg  6440  elmpt2cl  6499  1st2val  6807  2nd2val  6808  brovpreldm  6861  bropopvvv  6862  bropfvvvvlem  6863  ovmptss  6865  oprab2co  6869  curry1  6876  curry2  6879  algrflem  6893  mpt2xeldm  6945  mpt2xopn0yelv  6947  mpt2xopxnop0  6949  ovtpos  6975  mpt2curryd  7003  seqomlem1  7154  seqomlem4  7157  brwitnlem  7196  cantnfvalf  8157  fseqenlem1  8442  axdc4lem  8872  fpwwe  9058  canthwelem  9062  addpiord  9296  mulpiord  9297  addpqnq  9350  mulpqnq  9353  recmulnq  9376  dmrecnq  9380  cnref1o  11287  ixxssxr  11637  om2uzrdg  12164  uzrdgsuci  12168  swrd00  12773  swrd0  12789  cnrecnv  13239  sadcf  14438  smupf  14463  eucalgval  14552  eucalginv  14554  eucalglt  14555  eucalg  14557  vdwmc  14939  isstruct2  15141  isstruct  15142  imasaddvallem  15446  imasvscafn  15454  imasvscaval  15455  xpsff1o  15485  xpsaddlem  15492  xpsvsca  15496  xpsle  15498  comffval  15615  comfffval2  15617  comfeq  15622  isoval  15681  brcic  15714  isssc  15736  isfuncd  15781  funcf2  15784  idfu2nd  15793  idfucl  15797  cofucl  15804  resfval2  15809  resf2nd  15811  funcres2b  15813  funcpropd  15816  homarcl  15934  homaval  15937  homarcl2  15941  arwhoma  15951  coapm  15977  catcco  16007  catcisolem  16012  xpcco  16079  xpcid  16085  xpcpropd  16104  evlfcllem  16117  evlfcl  16118  curf1cl  16124  curf2cl  16127  curfcl  16128  uncf1  16132  uncf2  16133  uncfcurf  16135  diag11  16139  diag12  16140  diag2  16141  curf2ndf  16143  hof2fval  16151  hofcl  16155  hofpropd  16163  yonedalem21  16169  yonedalem22  16174  yonedalem3b  16175  yonedalem3  16176  yonedainv  16177  yonffthlem  16178  joinval  16262  meetval  16276  plusffval  16504  mgm1  16511  sgrp1  16545  mnd1  16588  mnd1OLD  16589  mnd1id  16590  grp1  16769  gaid  16964  oppglsm  17305  efgmnvl  17375  efgval2  17385  vrgpinv  17430  frgpuptinv  17432  frgpuplem  17433  frgpup2  17437  frgpup3lem  17438  frgpnabllem1  17520  gsum2dlem1  17613  gsum2dlem2  17614  gsum2d  17615  gsum2d2lem  17616  gsumcom2  17618  eldprd  17647  dprd2dlem2  17684  dprd2dlem1  17685  dprd2da  17686  ring1  17841  scaffval  18120  ply1frcl  18918  ipffval  19226  mamudi  19439  mamudir  19440  mamuvs1  19441  mamuvs2  19442  matplusgcell  19469  matsubgcell  19470  matvscacell  19472  mat1dimmul  19512  mat1rhmelval  19516  mdetrlin  19638  mdetrsca  19639  pmatcoe1fsupp  19736  iccordt  20241  iscnp2  20266  ptbasfi  20607  txcnpi  20634  txdis1cn  20661  lmcn2  20675  xkococn  20686  cnmpt12f  20692  cnmpt21  20697  cnmpt2t  20699  cnmpt22  20700  cnmpt2k  20714  xkohmeo  20841  flfcnp2  21033  tmdcn2  21115  clssubg  21134  tgphaus  21142  qustgplem  21146  psmetxrge0  21340  imasdsf1olem  21399  xpsdsval  21407  xmeterval  21458  comet  21539  txmetcnp  21573  metustid  21580  metustsym  21581  metustexhalf  21582  blval2  21588  metuel2  21591  nrmmetd  21600  nmfval  21614  isngp3  21623  ngpds  21628  tngnm  21670  qtopbaslem  21790  cnmetdval  21802  remetdval  21818  tgqioo  21829  bndth  21997  htpyco2  22021  phtpyco2  22032  caubl  22288  caublcls  22289  bcthlem1  22303  bcthlem2  22304  bcthlem4  22306  bcthlem5  22307  ovolfioo  22431  ovolficc  22432  ovolficcss  22433  ovolfsval  22434  ovolctb  22454  ovoliunlem2  22467  ovolicc2lem1  22481  ovolicc2lem5  22486  ovolfs2  22535  ioorinv  22540  ioorinvOLD  22545  uniiccdif  22547  uniioovol  22548  uniiccvol  22549  uniioombllem2a  22551  uniioombllem2  22552  uniioombllem2OLD  22553  uniioombllem3a  22554  uniioombllem3  22555  uniioombllem4  22556  uniioombllem5  22557  uniioombllem6  22558  dyadovol  22563  dyadss  22564  dyaddisjlem  22565  dyadmaxlem  22567  dyadmbl  22570  opnmbllem  22571  itg1addlem4  22669  limccnp2  22859  dvbsss  22869  perfdvf  22870  dvdsmulf1o  24135  fsumdvdsmul  24136  fsumvma  24153  tglngne  24607  ltgseg  24653  tgelrnln  24687  edgov  25080  usgraexmplvtx  25142  usgraexmplcvtx  25145  usgraexmplcedg  25146  2wlkonot3v  25615  2spthonot3v  25616  isrgrac  25674  grposn  25955  rngosn  26144  imsdval  26330  ofresid  28252  ofoprabco  28275  xrofsup  28361  smatrcl  28629  smatlem  28630  fvproj  28666  elunirnmbfm  29081  sibfof  29179  oddpwdcv  29194  eulerpartlemgh  29217  cndprobval  29272  cvmlift2lem9  30040  cvmlift2lem10  30041  cvmlift2lem13  30044  cvmliftphtlem  30046  mclsrcl  30205  fvtransport  30805  fvray  30914  linedegen  30916  fvline  30917  bj-finsumval0  31704  icoreunrn  31764  relowlpssretop  31769  finxpreclem1  31783  finxpreclem2  31784  finxpreclem3  31787  finxpreclem5  31789  opnmbllem0  31978  mblfinlem1  31979  mblfinlem2  31980  ftc1anc  32027  ftc2nc  32028  opropabco  32052  f1opr  32053  ismtyhmeolem  32138  heiborlem3  32147  heiborlem4  32148  heiborlem6  32150  heiborlem8  32152  fvovco  37479  volioof  37907  fvvolioof  37909  fvvolicof  37911  fourierdlem42  38069  fourierdlem42OLD  38070  hoi2toco  38492  ovolval2lem  38528  ovolval3  38532  ovolval4lem1  38534  ovolval5lem2  38538  ovnovollem1  38541  ovnovollem2  38542  aovfundmoveq  38774  aovpcov0  38783  aovnuoveq  38784  aovvoveq  38785  aov0ov0  38786  aovovn0oveq  38787  aov0nbovbi  38788  aovov0bi  38789  pfx00  39018  pfx0  39019  opvtxov  39207  opiedgov  39210  edgaov  39314  uhgrasize  40030  usgrafisbaseALT  40077  usgrafisbaseALT2  40078  usgfis  40083  usgfisALT  40087  ovn0dmfun  40089  ovn0ssdmfun  40092  plusfreseq  40097  idfusubc0  40190  rhmsubclem2  40414  rhmsubcALTVlem2  40433  lmod1lem2  40606  lmod1lem3  40607  logb2aval  40818
  Copyright terms: Public domain W3C validator