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

Definition df-ov 7287
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 𝐹 and its arguments 𝐴 and 𝐵- will be useful for proving meaningful theorems. For example, if class 𝐹 is the operation + and arguments 𝐴 and 𝐵 are 3 and 2, the expression (3 + 2) can be proved to equal 5 (see 3p2e5 12133). This definition is well-defined, although not very meaningful, when classes 𝐴 and/or 𝐵 are proper classes (i.e. are not sets); see ovprc1 7323 and ovprc2 7324. On the other hand, we often find uses for this definition when 𝐹 is a proper class, such as +o in oav 8350. 𝐹 is normally equal to a class of nested ordered pairs of the form defined by df-oprab 7288. (Contributed by NM, 28-Feb-1995.)
Assertion
Ref Expression
df-ov (𝐴𝐹𝐵) = (𝐹‘⟨𝐴, 𝐵⟩)

Detailed syntax breakdown of Definition df-ov
StepHypRef Expression
1 cA . . 3 class 𝐴
2 cB . . 3 class 𝐵
3 cF . . 3 class 𝐹
41, 2, 3co 7284 . 2 class (𝐴𝐹𝐵)
51, 2cop 4568 . . 3 class 𝐴, 𝐵
65, 3cfv 6437 . 2 class (𝐹‘⟨𝐴, 𝐵⟩)
74, 6wceq 1539 1 wff (𝐴𝐹𝐵) = (𝐹‘⟨𝐴, 𝐵⟩)
Colors of variables: wff setvar class
This definition is referenced by:  oveq  7290  oveq1  7291  oveq2  7292  nfovd  7313  ovex  7317  ovssunirn  7320  0ov  7321  ovprc  7322  csbov123  7326  csbov  7327  elovimad  7332  fnbrovb  7333  f1opr  7340  ffnov  7410  eqfnov  7412  fnov  7414  ovid  7423  ovidig  7424  ov  7426  ovigg  7427  fvmpopr2d  7443  ov6g  7445  ovg  7446  ovres  7447  fovrn  7451  fnrnov  7454  foov  7455  fnovrn  7456  funimassov  7458  ovelimab  7459  ovima0  7460  ovconst2  7461  oprssdm  7462  nssdmovg  7463  ndmovg  7464  elmpocl  7520  1st2val  7868  2nd2val  7869  brovpreldm  7938  bropopvvv  7939  bropfvvvvlem  7940  ovmptss  7942  oprab2co  7946  curry1  7953  curry2  7956  fsplitfpar  7968  offsplitfpar  7969  opco1  7973  opco2  7974  fvproj  7984  mpoxeldm  8036  mpoxopn0yelv  8038  mpoxopxnop0  8040  ovtpos  8066  mpocurryd  8094  seqomlem1  8290  seqomlem4  8293  brwitnlem  8346  cantnfvalf  9432  fseqenlem1  9789  axdc4lem  10220  fpwwe  10411  canthwelem  10415  addpiord  10649  mulpiord  10650  addpqnq  10703  mulpqnq  10706  recmulnq  10729  dmrecnq  10733  cnref1o  12734  ixxssxr  13100  om2uzrdg  13685  uzrdgsuci  13689  seqexw  13746  swrd00  14366  swrd0  14380  pfx00  14396  pfx0  14397  cnrecnv  14885  sadcf  16169  smupf  16194  eucalgval  16296  eucalginv  16298  eucalglt  16299  eucalg  16301  vdwmc  16688  isstruct2  16859  isstruct  16862  setsstruct2  16884  imasaddvallem  17249  imasvscafn  17257  imasvscaval  17258  xpsff1o  17287  xpsaddlem  17293  xpsvsca  17297  xpsle  17299  comffval  17417  comfffval2  17419  comfeq  17424  isoval  17486  brcic  17519  isssc  17541  isfuncd  17589  funcf2  17592  idfu2nd  17601  idfucl  17605  cofucl  17612  resfval2  17617  resf2nd  17619  funcres2b  17621  funcpropd  17625  homaval  17755  homarcl2  17759  arwhoma  17769  coapm  17795  catcco  17829  catcisolem  17834  xpcco  17909  xpcid  17915  xpcpropd  17935  evlfcllem  17948  evlfcl  17949  curf1cl  17955  curf2cl  17958  curfcl  17959  uncf1  17963  uncf2  17964  uncfcurf  17966  diag11  17970  diag12  17971  diag2  17972  curf2ndf  17974  hof2fval  17982  hofcl  17986  hofpropd  17994  yonedalem21  18000  yonedalem22  18005  yonedalem3b  18006  yonedalem3  18007  yonedainv  18008  yonffthlem  18009  joinval  18104  meetval  18118  plusffval  18341  mgm1  18351  sgrp1  18393  mnd1  18435  mnd1id  18436  grpsubfval  18632  grp1  18691  mulgfval  18711  gaid  18914  efgmnvl  19329  efgval2  19339  vrgpinv  19384  frgpuptinv  19386  frgpuplem  19387  frgpup2  19391  frgpup3lem  19392  frgpnabllem1  19483  gsum2dlem1  19580  gsum2dlem2  19581  gsum2d  19582  gsum2d2lem  19583  gsumcom2  19585  gsumxp2  19590  eldprd  19616  dprd2dlem2  19652  dprd2dlem1  19653  dprd2da  19654  srgfcl  19760  ring1  19850  scaffval  20150  ipffval  20862  ply1frcl  21493  mamudi  21559  mamudir  21560  mamuvs1  21561  mamuvs2  21562  matplusgcell  21591  matsubgcell  21592  matvscacell  21594  mat1dimmul  21634  mat1rhmelval  21638  mdetrlin  21760  mdetrsca  21761  pmatcoe1fsupp  21859  iccordt  22374  iscnp2  22399  ptbasfi  22741  txcnpi  22768  txdis1cn  22795  lmcn2  22809  xkococn  22820  cnmpt12f  22826  cnmpt21  22831  cnmpt2t  22833  cnmpt22  22834  cnmpt2k  22848  xkohmeo  22975  flfcnp2  23167  tmdcn2  23249  clssubg  23269  tgphaus  23277  qustgplem  23281  psmetxrge0  23475  imasdsf1olem  23535  xpsdsval  23543  xmeterval  23594  comet  23678  txmetcnp  23712  metustid  23719  metustsym  23720  metustexhalf  23721  blval2  23727  metuel2  23730  nrmmetd  23739  nmfval  23753  isngp3  23763  ngpds  23769  tngnm  23824  qtopbaslem  23931  cnmetdval  23943  remetdval  23961  tgqioo  23972  bndth  24130  htpyco2  24151  phtpyco2  24162  caubl  24481  caublcls  24482  bcthlem1  24497  bcthlem2  24498  bcthlem4  24500  bcthlem5  24501  ovolfioo  24640  ovolficc  24641  ovolficcss  24642  ovolfsval  24643  ovolctb  24663  ovoliunlem2  24676  ovolicc2lem1  24690  ovolicc2lem5  24694  ovolfs2  24744  ioorinv  24749  uniiccdif  24751  uniioovol  24752  uniiccvol  24753  uniioombllem2a  24755  uniioombllem2  24756  uniioombllem3a  24757  uniioombllem3  24758  uniioombllem4  24759  uniioombllem5  24760  uniioombllem6  24761  dyadovol  24766  dyadss  24767  dyaddisjlem  24768  dyadmaxlem  24770  dyadmbl  24773  opnmbllem  24774  itg1addlem4  24872  itg1addlem4OLD  24873  limccnp2  25065  dvbsss  25075  perfdvf  25076  dvdsmulf1o  26352  fsumdvdsmul  26353  fsumvma  26370  tgjustc1  26845  tgjustc2  26846  tglngne  26920  ltgseg  26966  tgelrnln  27000  opvtxov  27384  opiedgov  27387  edgov  27431  vtxdgop  27846  finsumvtxdg2size  27926  ex-fpar  28835  imsdval  29057  ofresid  30988  ofoprabco  31010  suppovss  31026  fsuppcurry1  31069  fsuppcurry2  31070  xrofsup  31099  gsumpart  31324  fedgmullem2  31720  smatrcl  31755  smatlem  31756  elunirnmbfm  32229  sibfof  32316  oddpwdcv  32331  eulerpartlemgh  32354  cndprobval  32409  cvmlift2lem9  33282  cvmlift2lem10  33283  cvmlift2lem13  33286  cvmliftphtlem  33288  goel  33318  gonafv  33321  sat1el2xp  33350  on2recsov  33836  madeval2  34046  scutfo  34093  norec2ov  34123  addsval  34135  fvtransport  34343  fvray  34452  linedegen  34454  fvline  34455  bj-finsumval0  35465  icoreunrn  35539  relowlpssretop  35544  finxpreclem1  35569  finxpreclem2  35570  finxpreclem3  35573  finxpreclem5  35575  curfv  35766  uncov  35767  curunc  35768  opnmbllem0  35822  mblfinlem1  35823  mblfinlem2  35824  ftc1anc  35867  ftc2nc  35868  opropabco  35891  ismtyhmeolem  35971  heiborlem3  35980  heiborlem4  35981  heiborlem6  35983  heiborlem8  35985  grposnOLD  36049  fvovco  42739  volioof  43535  fvvolioof  43537  fvvolicof  43539  fourierdlem42  43697  hoi2toco  44152  ovolval2lem  44188  ovolval3  44192  ovolval4lem1  44194  ovolval5lem2  44198  ovnovollem1  44201  ovnovollem2  44202  smfpimbor1lem1  44343  aovfundmoveq  44684  aovpcov0  44693  aovnuoveq  44694  aovvoveq  44695  aov0ov0  44696  aovovn0oveq  44697  aov0nbovbi  44698  aovov0bi  44699  ovn0dmfun  45329  ovn0ssdmfun  45332  plusfreseq  45337  idfusubc0  45434  rhmsubclem2  45656  rhmsubcALTVlem2  45674  lmod1lem2  45840  lmod1lem3  45841  rrx2xpref1o  46075  rrx2plordisom  46080  fvconstr  46194  fvconstrn0  46195  fvconstr2  46196  funcf2lem  46310  indthinc  46344  prsthinc  46346  mndtchom  46382  mndtcco  46383  logb2aval  46477
  Copyright terms: Public domain W3C validator