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 7216
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 11981). This definition is well-defined, although not very meaningful, when classes 𝐴 and/or 𝐵 are proper classes (i.e. are not sets); see ovprc1 7252 and ovprc2 7253. On the other hand, we often find uses for this definition when 𝐹 is a proper class, such as +o in oav 8238. 𝐹 is normally equal to a class of nested ordered pairs of the form defined by df-oprab 7217. (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 7213 . 2 class (𝐴𝐹𝐵)
51, 2cop 4547 . . 3 class 𝐴, 𝐵
65, 3cfv 6380 . 2 class (𝐹‘⟨𝐴, 𝐵⟩)
74, 6wceq 1543 1 wff (𝐴𝐹𝐵) = (𝐹‘⟨𝐴, 𝐵⟩)
Colors of variables: wff setvar class
This definition is referenced by:  oveq  7219  oveq1  7220  oveq2  7221  nfovd  7242  ovex  7246  ovssunirn  7249  0ov  7250  ovprc  7251  csbov123  7255  csbov  7256  elovimad  7261  fnbrovb  7262  f1opr  7267  ffnov  7337  eqfnov  7339  fnov  7341  ovid  7350  ovidig  7351  ov  7353  ovigg  7354  fvmpopr2d  7370  ov6g  7372  ovg  7373  ovres  7374  fovrn  7378  fnrnov  7381  foov  7382  fnovrn  7383  funimassov  7385  ovelimab  7386  ovima0  7387  ovconst2  7388  oprssdm  7389  nssdmovg  7390  ndmovg  7391  elmpocl  7447  1st2val  7789  2nd2val  7790  brovpreldm  7857  bropopvvv  7858  bropfvvvvlem  7859  ovmptss  7861  oprab2co  7865  curry1  7872  curry2  7875  fsplitfpar  7887  offsplitfpar  7888  algrflem  7892  fvproj  7901  mpoxeldm  7953  mpoxopn0yelv  7955  mpoxopxnop0  7957  ovtpos  7983  mpocurryd  8011  seqomlem1  8186  seqomlem4  8189  brwitnlem  8234  cantnfvalf  9280  fseqenlem1  9638  axdc4lem  10069  fpwwe  10260  canthwelem  10264  addpiord  10498  mulpiord  10499  addpqnq  10552  mulpqnq  10555  recmulnq  10578  dmrecnq  10582  cnref1o  12581  ixxssxr  12947  om2uzrdg  13529  uzrdgsuci  13533  seqexw  13590  swrd00  14209  swrd0  14223  pfx00  14239  pfx0  14240  cnrecnv  14728  sadcf  16012  smupf  16037  eucalgval  16139  eucalginv  16141  eucalglt  16142  eucalg  16144  vdwmc  16531  isstruct2  16702  isstruct  16705  setsstruct2  16727  imasaddvallem  17034  imasvscafn  17042  imasvscaval  17043  xpsff1o  17072  xpsaddlem  17078  xpsvsca  17082  xpsle  17084  comffval  17202  comfffval2  17204  comfeq  17209  isoval  17270  brcic  17303  isssc  17325  isfuncd  17371  funcf2  17374  idfu2nd  17383  idfucl  17387  cofucl  17394  resfval2  17399  resf2nd  17401  funcres2b  17403  funcpropd  17407  homaval  17537  homarcl2  17541  arwhoma  17551  coapm  17577  catcco  17611  catcisolem  17616  xpcco  17690  xpcid  17696  xpcpropd  17716  evlfcllem  17729  evlfcl  17730  curf1cl  17736  curf2cl  17739  curfcl  17740  uncf1  17744  uncf2  17745  uncfcurf  17747  diag11  17751  diag12  17752  diag2  17753  curf2ndf  17755  hof2fval  17763  hofcl  17767  hofpropd  17775  yonedalem21  17781  yonedalem22  17786  yonedalem3b  17787  yonedalem3  17788  yonedainv  17789  yonffthlem  17790  joinval  17883  meetval  17897  plusffval  18120  mgm1  18130  sgrp1  18172  mnd1  18214  mnd1id  18215  grpsubfval  18411  grp1  18470  mulgfval  18490  gaid  18693  efgmnvl  19104  efgval2  19114  vrgpinv  19159  frgpuptinv  19161  frgpuplem  19162  frgpup2  19166  frgpup3lem  19167  frgpnabllem1  19258  gsum2dlem1  19355  gsum2dlem2  19356  gsum2d  19357  gsum2d2lem  19358  gsumcom2  19360  gsumxp2  19365  eldprd  19391  dprd2dlem2  19427  dprd2dlem1  19428  dprd2da  19429  srgfcl  19530  ring1  19620  scaffval  19917  ipffval  20610  ply1frcl  21234  mamudi  21300  mamudir  21301  mamuvs1  21302  mamuvs2  21303  matplusgcell  21330  matsubgcell  21331  matvscacell  21333  mat1dimmul  21373  mat1rhmelval  21377  mdetrlin  21499  mdetrsca  21500  pmatcoe1fsupp  21598  iccordt  22111  iscnp2  22136  ptbasfi  22478  txcnpi  22505  txdis1cn  22532  lmcn2  22546  xkococn  22557  cnmpt12f  22563  cnmpt21  22568  cnmpt2t  22570  cnmpt22  22571  cnmpt2k  22585  xkohmeo  22712  flfcnp2  22904  tmdcn2  22986  clssubg  23006  tgphaus  23014  qustgplem  23018  psmetxrge0  23211  imasdsf1olem  23271  xpsdsval  23279  xmeterval  23330  comet  23411  txmetcnp  23445  metustid  23452  metustsym  23453  metustexhalf  23454  blval2  23460  metuel2  23463  nrmmetd  23472  nmfval  23486  isngp3  23496  ngpds  23502  tngnm  23549  qtopbaslem  23656  cnmetdval  23668  remetdval  23686  tgqioo  23697  bndth  23855  htpyco2  23876  phtpyco2  23887  caubl  24205  caublcls  24206  bcthlem1  24221  bcthlem2  24222  bcthlem4  24224  bcthlem5  24225  ovolfioo  24364  ovolficc  24365  ovolficcss  24366  ovolfsval  24367  ovolctb  24387  ovoliunlem2  24400  ovolicc2lem1  24414  ovolicc2lem5  24418  ovolfs2  24468  ioorinv  24473  uniiccdif  24475  uniioovol  24476  uniiccvol  24477  uniioombllem2a  24479  uniioombllem2  24480  uniioombllem3a  24481  uniioombllem3  24482  uniioombllem4  24483  uniioombllem5  24484  uniioombllem6  24485  dyadovol  24490  dyadss  24491  dyaddisjlem  24492  dyadmaxlem  24494  dyadmbl  24497  opnmbllem  24498  itg1addlem4  24596  itg1addlem4OLD  24597  limccnp2  24789  dvbsss  24799  perfdvf  24800  dvdsmulf1o  26076  fsumdvdsmul  26077  fsumvma  26094  tgjustc1  26566  tgjustc2  26567  tglngne  26641  ltgseg  26687  tgelrnln  26721  opvtxov  27096  opiedgov  27099  edgov  27143  vtxdgop  27558  finsumvtxdg2size  27638  ex-fpar  28545  imsdval  28767  ofresid  30698  ofoprabco  30721  suppovss  30737  fsuppcurry1  30780  fsuppcurry2  30781  xrofsup  30810  gsumpart  31034  fedgmullem2  31425  smatrcl  31460  smatlem  31461  elunirnmbfm  31932  sibfof  32019  oddpwdcv  32034  eulerpartlemgh  32057  cndprobval  32112  cvmlift2lem9  32986  cvmlift2lem10  32987  cvmlift2lem13  32990  cvmliftphtlem  32992  goel  33022  gonafv  33025  sat1el2xp  33054  on2recsov  33564  madeval2  33774  scutfo  33821  norec2ov  33851  addsval  33863  fvtransport  34071  fvray  34180  linedegen  34182  fvline  34183  bj-finsumval0  35191  icoreunrn  35267  relowlpssretop  35272  finxpreclem1  35297  finxpreclem2  35298  finxpreclem3  35301  finxpreclem5  35303  curfv  35494  uncov  35495  curunc  35496  opnmbllem0  35550  mblfinlem1  35551  mblfinlem2  35552  ftc1anc  35595  ftc2nc  35596  opropabco  35619  ismtyhmeolem  35699  heiborlem3  35708  heiborlem4  35709  heiborlem6  35711  heiborlem8  35713  grposnOLD  35777  fvovco  42405  volioof  43203  fvvolioof  43205  fvvolicof  43207  fourierdlem42  43365  hoi2toco  43820  ovolval2lem  43856  ovolval3  43860  ovolval4lem1  43862  ovolval5lem2  43866  ovnovollem1  43869  ovnovollem2  43870  smfpimbor1lem1  44004  aovfundmoveq  44345  aovpcov0  44354  aovnuoveq  44355  aovvoveq  44356  aov0ov0  44357  aovovn0oveq  44358  aov0nbovbi  44359  aovov0bi  44360  ovn0dmfun  44991  ovn0ssdmfun  44994  plusfreseq  44999  idfusubc0  45096  rhmsubclem2  45318  rhmsubcALTVlem2  45336  lmod1lem2  45502  lmod1lem3  45503  rrx2xpref1o  45737  rrx2plordisom  45742  fvconstr  45856  fvconstrn0  45857  fvconstr2  45858  funcf2lem  45972  indthinc  46006  prsthinc  46008  mndtchom  46042  mndtcco  46043  logb2aval  46137
  Copyright terms: Public domain W3C validator