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 7434
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 12417). This definition is well-defined, although not very meaningful, when classes 𝐴 and/or 𝐵 are proper classes (i.e. are not sets); see ovprc1 7470 and ovprc2 7471. On the other hand, we often find uses for this definition when 𝐹 is a proper class, such as +o in oav 8549. 𝐹 is normally equal to a class of nested ordered pairs of the form defined by df-oprab 7435. (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 7431 . 2 class (𝐴𝐹𝐵)
51, 2cop 4632 . . 3 class 𝐴, 𝐵
65, 3cfv 6561 . 2 class (𝐹‘⟨𝐴, 𝐵⟩)
74, 6wceq 1540 1 wff (𝐴𝐹𝐵) = (𝐹‘⟨𝐴, 𝐵⟩)
Colors of variables: wff setvar class
This definition is referenced by:  oveq  7437  oveq1  7438  oveq2  7439  nfovd  7460  ovex  7464  ovssunirn  7467  0ov  7468  ovprc  7469  csbov123  7475  csbov  7476  elovimad  7481  fnbrovb  7482  f1opr  7489  ffnov  7559  eqfnov  7562  fnov  7564  ovid  7574  ovidig  7575  ov  7577  ovigg  7578  fvmpopr2d  7595  ov6g  7597  ovg  7598  ovres  7599  fovcdm  7603  fnrnov  7606  foov  7607  fnovrn  7608  funimassov  7610  ovelimab  7611  ovima0  7612  ovconst2  7613  oprssdm  7614  nssdmovg  7615  ndmovg  7616  elmpocl  7674  1st2val  8042  2nd2val  8043  brovpreldm  8114  bropopvvv  8115  bropfvvvvlem  8116  ovmptss  8118  oprab2co  8122  curry1  8129  curry2  8132  fsplitfpar  8143  offsplitfpar  8144  opco1  8148  opco2  8149  fvproj  8159  mpoxeldm  8236  mpoxopn0yelv  8238  mpoxopxnop0  8240  ovtpos  8266  mpocurryd  8294  seqomlem1  8490  seqomlem4  8493  brwitnlem  8545  on2recsov  8706  naddf  8719  cantnfvalf  9705  fseqenlem1  10064  axdc4lem  10495  fpwwe  10686  canthwelem  10690  addpiord  10924  mulpiord  10925  addpqnq  10978  mulpqnq  10981  recmulnq  11004  dmrecnq  11008  cnref1o  13027  ixxssxr  13399  om2uzrdg  13997  uzrdgsuci  14001  seqexw  14058  swrd00  14682  swrd0  14696  pfx00  14712  pfx0  14713  cnrecnv  15204  sadcf  16490  smupf  16515  eucalgval  16619  eucalginv  16621  eucalglt  16622  eucalg  16624  vdwmc  17016  isstruct2  17186  isstruct  17189  setsstruct2  17211  imasaddvallem  17574  imasvscafn  17582  imasvscaval  17583  xpsff1o  17612  xpsaddlem  17618  xpsvsca  17622  xpsle  17624  comffval  17742  comfffval2  17744  comfeq  17749  isoval  17809  brcic  17842  isssc  17864  isfuncd  17910  funcf2  17913  idfu2nd  17922  idfucl  17926  cofucl  17933  resfval2  17938  resf2nd  17940  funcres2b  17942  idfusubc0  17944  funcpropd  17947  homaval  18076  homarcl2  18080  arwhoma  18090  coapm  18116  catcco  18150  catcisolem  18155  xpcco  18228  xpcid  18234  xpcpropd  18253  evlfcllem  18266  evlfcl  18267  curf1cl  18273  curf2cl  18276  curfcl  18277  uncf1  18281  uncf2  18282  uncfcurf  18284  diag11  18288  diag12  18289  diag2  18290  curf2ndf  18292  hof2fval  18300  hofcl  18304  hofpropd  18312  yonedalem21  18318  yonedalem22  18323  yonedalem3b  18324  yonedalem3  18325  yonedainv  18326  yonffthlem  18327  joinval  18422  meetval  18436  plusffval  18659  mgm1  18671  sgrp1  18742  mnd1  18792  mnd1id  18793  grpsubfval  19001  grp1  19065  mulgfval  19087  gaid  19317  efgmnvl  19732  efgval2  19742  vrgpinv  19787  frgpuptinv  19789  frgpuplem  19790  frgpup2  19794  frgpup3lem  19795  frgpnabllem1  19891  gsum2dlem1  19988  gsum2dlem2  19989  gsum2d  19990  gsum2d2lem  19991  gsumcom2  19993  gsumxp2  19998  eldprd  20024  dprd2dlem2  20060  dprd2dlem1  20061  dprd2da  20062  srgfcl  20193  ring1  20307  rhmsubclem2  20686  scaffval  20878  ipffval  21666  ply1frcl  22322  mamudi  22407  mamudir  22408  mamuvs1  22409  mamuvs2  22410  matplusgcell  22439  matsubgcell  22440  matvscacell  22442  mat1dimmul  22482  mat1rhmelval  22486  mdetrlin  22608  mdetrsca  22609  pmatcoe1fsupp  22707  iccordt  23222  iscnp2  23247  ptbasfi  23589  txcnpi  23616  txdis1cn  23643  lmcn2  23657  xkococn  23668  cnmpt12f  23674  cnmpt21  23679  cnmpt2t  23681  cnmpt22  23682  cnmpt2k  23696  xkohmeo  23823  flfcnp2  24015  tmdcn2  24097  clssubg  24117  tgphaus  24125  qustgplem  24129  psmetxrge0  24323  imasdsf1olem  24383  xpsdsval  24391  xmeterval  24442  comet  24526  txmetcnp  24560  metustid  24567  metustsym  24568  metustexhalf  24569  blval2  24575  metuel2  24578  nrmmetd  24587  nmfval  24601  isngp3  24611  ngpds  24617  tngnm  24672  qtopbaslem  24779  cnmetdval  24791  remetdval  24810  tgqioo  24821  mpomulcn  24891  bndth  24990  htpyco2  25011  phtpyco2  25022  caubl  25342  caublcls  25343  bcthlem1  25358  bcthlem2  25359  bcthlem4  25361  bcthlem5  25362  ovolfioo  25502  ovolficc  25503  ovolficcss  25504  ovolfsval  25505  ovolctb  25525  ovoliunlem2  25538  ovolicc2lem1  25552  ovolicc2lem5  25556  ovolfs2  25606  ioorinv  25611  uniiccdif  25613  uniioovol  25614  uniiccvol  25615  uniioombllem2a  25617  uniioombllem2  25618  uniioombllem3a  25619  uniioombllem3  25620  uniioombllem4  25621  uniioombllem5  25622  uniioombllem6  25623  dyadovol  25628  dyadss  25629  dyaddisjlem  25630  dyadmaxlem  25632  dyadmbl  25635  opnmbllem  25636  itg1addlem4  25734  limccnp2  25927  dvbsss  25937  perfdvf  25938  mpodvdsmulf1o  27237  fsumdvdsmul  27238  dvdsmulf1o  27239  fsumdvdsmulOLD  27240  fsumvma  27257  madeval2  27892  scutfo  27942  norec2ov  27990  addsval  27995  addsf  28015  addsfo  28016  subsfo  28095  mulsval  28135  om2noseqrdg  28310  noseqrdgsuc  28314  tgjustc1  28483  tgjustc2  28484  tglngne  28558  ltgseg  28604  tgelrnln  28638  opvtxov  29022  opiedgov  29025  edgov  29069  vtxdgop  29488  finsumvtxdg2size  29568  ex-fpar  30481  imsdval  30705  ofresid  32652  ofoprabco  32674  suppovss  32690  fsuppcurry1  32736  fsuppcurry2  32737  xrofsup  32771  gsumpart  33060  elrgspnlem2  33247  fedgmullem2  33681  smatrcl  33795  smatlem  33796  elunirnmbfm  34253  sibfof  34342  oddpwdcv  34357  eulerpartlemgh  34380  cndprobval  34435  cvmlift2lem9  35316  cvmlift2lem10  35317  cvmlift2lem13  35320  cvmliftphtlem  35322  goel  35352  gonafv  35355  sat1el2xp  35384  fvtransport  36033  fvray  36142  linedegen  36144  fvline  36145  bj-finsumval0  37286  icoreunrn  37360  relowlpssretop  37365  finxpreclem1  37390  finxpreclem2  37391  finxpreclem3  37394  finxpreclem5  37396  curfv  37607  uncov  37608  curunc  37609  opnmbllem0  37663  mblfinlem1  37664  mblfinlem2  37665  ftc1anc  37708  ftc2nc  37709  opropabco  37731  ismtyhmeolem  37811  heiborlem3  37820  heiborlem4  37821  heiborlem6  37823  heiborlem8  37825  grposnOLD  37889  fvovco  45198  volioof  46002  fvvolioof  46004  fvvolicof  46006  fourierdlem42  46164  hoi2toco  46622  ovolval2lem  46658  ovolval3  46662  ovolval4lem1  46664  ovolval5lem2  46668  ovnovollem1  46671  ovnovollem2  46672  smfpimbor1lem1  46813  aovfundmoveq  47193  aovpcov0  47202  aovnuoveq  47203  aovvoveq  47204  aov0ov0  47205  aovovn0oveq  47206  aov0nbovbi  47207  aovov0bi  47208  ovn0dmfun  48072  ovn0ssdmfun  48075  plusfreseq  48080  rhmsubcALTVlem2  48198  lmod1lem2  48405  lmod1lem3  48406  rrx2xpref1o  48639  rrx2plordisom  48644  fvconstr  48765  fvconstrn0  48766  fvconstr2  48767  tposid  48785  tposidres  48786  tposideq  48788  funcf2lem  48914  swapf1  48978  swapf2  48980  swapfid  48985  cofuswapf1  48994  cofuswapf2  48995  fucofulem2  49006  fucofvalne  49020  fuco11  49021  fuco11bALT  49033  fucoid  49043  fucocolem2  49049  fucocolem4  49051  precofvalALT  49063  indthinc  49109  prsthinc  49111  mndtchom  49181  mndtcco  49182  logb2aval  49283
  Copyright terms: Public domain W3C validator