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 7409
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 12360). This definition is well-defined, although not very meaningful, when classes 𝐴 and/or 𝐵 are proper classes (i.e. are not sets); see ovprc1 7445 and ovprc2 7446. On the other hand, we often find uses for this definition when 𝐹 is a proper class, such as +o in oav 8508. 𝐹 is normally equal to a class of nested ordered pairs of the form defined by df-oprab 7410. (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 7406 . 2 class (𝐴𝐹𝐵)
51, 2cop 4634 . . 3 class 𝐴, 𝐵
65, 3cfv 6541 . 2 class (𝐹‘⟨𝐴, 𝐵⟩)
74, 6wceq 1542 1 wff (𝐴𝐹𝐵) = (𝐹‘⟨𝐴, 𝐵⟩)
Colors of variables: wff setvar class
This definition is referenced by:  oveq  7412  oveq1  7413  oveq2  7414  nfovd  7435  ovex  7439  ovssunirn  7442  0ov  7443  ovprc  7444  csbov123  7448  csbov  7449  elovimad  7454  fnbrovb  7455  f1opr  7462  ffnov  7532  eqfnov  7535  fnov  7537  ovid  7546  ovidig  7547  ov  7549  ovigg  7550  fvmpopr2d  7566  ov6g  7568  ovg  7569  ovres  7570  fovcdm  7574  fnrnov  7577  foov  7578  fnovrn  7579  funimassov  7581  ovelimab  7582  ovima0  7583  ovconst2  7584  oprssdm  7585  nssdmovg  7586  ndmovg  7587  elmpocl  7645  1st2val  8000  2nd2val  8001  brovpreldm  8072  bropopvvv  8073  bropfvvvvlem  8074  ovmptss  8076  oprab2co  8080  curry1  8087  curry2  8090  fsplitfpar  8101  offsplitfpar  8102  opco1  8106  opco2  8107  fvproj  8117  mpoxeldm  8193  mpoxopn0yelv  8195  mpoxopxnop0  8197  ovtpos  8223  mpocurryd  8251  seqomlem1  8447  seqomlem4  8450  brwitnlem  8504  on2recsov  8664  naddf  8677  cantnfvalf  9657  fseqenlem1  10016  axdc4lem  10447  fpwwe  10638  canthwelem  10642  addpiord  10876  mulpiord  10877  addpqnq  10930  mulpqnq  10933  recmulnq  10956  dmrecnq  10960  cnref1o  12966  ixxssxr  13333  om2uzrdg  13918  uzrdgsuci  13922  seqexw  13979  swrd00  14591  swrd0  14605  pfx00  14621  pfx0  14622  cnrecnv  15109  sadcf  16391  smupf  16416  eucalgval  16516  eucalginv  16518  eucalglt  16519  eucalg  16521  vdwmc  16908  isstruct2  17079  isstruct  17082  setsstruct2  17104  imasaddvallem  17472  imasvscafn  17480  imasvscaval  17481  xpsff1o  17510  xpsaddlem  17516  xpsvsca  17520  xpsle  17522  comffval  17640  comfffval2  17642  comfeq  17647  isoval  17709  brcic  17742  isssc  17764  isfuncd  17812  funcf2  17815  idfu2nd  17824  idfucl  17828  cofucl  17835  resfval2  17840  resf2nd  17842  funcres2b  17844  funcpropd  17848  homaval  17978  homarcl2  17982  arwhoma  17992  coapm  18018  catcco  18052  catcisolem  18057  xpcco  18132  xpcid  18138  xpcpropd  18158  evlfcllem  18171  evlfcl  18172  curf1cl  18178  curf2cl  18181  curfcl  18182  uncf1  18186  uncf2  18187  uncfcurf  18189  diag11  18193  diag12  18194  diag2  18195  curf2ndf  18197  hof2fval  18205  hofcl  18209  hofpropd  18217  yonedalem21  18223  yonedalem22  18228  yonedalem3b  18229  yonedalem3  18230  yonedainv  18231  yonffthlem  18232  joinval  18327  meetval  18341  plusffval  18564  mgm1  18574  sgrp1  18617  mnd1  18664  mnd1id  18665  grpsubfval  18865  grp1  18927  mulgfval  18947  gaid  19158  efgmnvl  19577  efgval2  19587  vrgpinv  19632  frgpuptinv  19634  frgpuplem  19635  frgpup2  19639  frgpup3lem  19640  frgpnabllem1  19736  gsum2dlem1  19833  gsum2dlem2  19834  gsum2d  19835  gsum2d2lem  19836  gsumcom2  19838  gsumxp2  19843  eldprd  19869  dprd2dlem2  19905  dprd2dlem1  19906  dprd2da  19907  srgfcl  20013  ring1  20116  scaffval  20483  ipffval  21193  ply1frcl  21829  mamudi  21895  mamudir  21896  mamuvs1  21897  mamuvs2  21898  matplusgcell  21927  matsubgcell  21928  matvscacell  21930  mat1dimmul  21970  mat1rhmelval  21974  mdetrlin  22096  mdetrsca  22097  pmatcoe1fsupp  22195  iccordt  22710  iscnp2  22735  ptbasfi  23077  txcnpi  23104  txdis1cn  23131  lmcn2  23145  xkococn  23156  cnmpt12f  23162  cnmpt21  23167  cnmpt2t  23169  cnmpt22  23170  cnmpt2k  23184  xkohmeo  23311  flfcnp2  23503  tmdcn2  23585  clssubg  23605  tgphaus  23613  qustgplem  23617  psmetxrge0  23811  imasdsf1olem  23871  xpsdsval  23879  xmeterval  23930  comet  24014  txmetcnp  24048  metustid  24055  metustsym  24056  metustexhalf  24057  blval2  24063  metuel2  24066  nrmmetd  24075  nmfval  24089  isngp3  24099  ngpds  24105  tngnm  24160  qtopbaslem  24267  cnmetdval  24279  remetdval  24297  tgqioo  24308  bndth  24466  htpyco2  24487  phtpyco2  24498  caubl  24817  caublcls  24818  bcthlem1  24833  bcthlem2  24834  bcthlem4  24836  bcthlem5  24837  ovolfioo  24976  ovolficc  24977  ovolficcss  24978  ovolfsval  24979  ovolctb  24999  ovoliunlem2  25012  ovolicc2lem1  25026  ovolicc2lem5  25030  ovolfs2  25080  ioorinv  25085  uniiccdif  25087  uniioovol  25088  uniiccvol  25089  uniioombllem2a  25091  uniioombllem2  25092  uniioombllem3a  25093  uniioombllem3  25094  uniioombllem4  25095  uniioombllem5  25096  uniioombllem6  25097  dyadovol  25102  dyadss  25103  dyaddisjlem  25104  dyadmaxlem  25106  dyadmbl  25109  opnmbllem  25110  itg1addlem4  25208  itg1addlem4OLD  25209  limccnp2  25401  dvbsss  25411  perfdvf  25412  dvdsmulf1o  26688  fsumdvdsmul  26689  fsumvma  26706  madeval2  27338  scutfo  27388  norec2ov  27431  addsval  27436  addsf  27456  addsfo  27457  mulsval  27555  tgjustc1  27716  tgjustc2  27717  tglngne  27791  ltgseg  27837  tgelrnln  27871  opvtxov  28255  opiedgov  28258  edgov  28302  vtxdgop  28717  finsumvtxdg2size  28797  ex-fpar  29705  imsdval  29927  ofresid  31855  ofoprabco  31877  suppovss  31894  fsuppcurry1  31938  fsuppcurry2  31939  xrofsup  31968  gsumpart  32195  fedgmullem2  32704  smatrcl  32765  smatlem  32766  elunirnmbfm  33239  sibfof  33328  oddpwdcv  33343  eulerpartlemgh  33366  cndprobval  33421  cvmlift2lem9  34291  cvmlift2lem10  34292  cvmlift2lem13  34295  cvmliftphtlem  34297  goel  34327  gonafv  34330  sat1el2xp  34359  fvtransport  34993  fvray  35102  linedegen  35104  fvline  35105  mpomulcn  35151  bj-finsumval0  36155  icoreunrn  36229  relowlpssretop  36234  finxpreclem1  36259  finxpreclem2  36260  finxpreclem3  36263  finxpreclem5  36265  curfv  36457  uncov  36458  curunc  36459  opnmbllem0  36513  mblfinlem1  36514  mblfinlem2  36515  ftc1anc  36558  ftc2nc  36559  opropabco  36581  ismtyhmeolem  36661  heiborlem3  36670  heiborlem4  36671  heiborlem6  36673  heiborlem8  36675  grposnOLD  36739  fvovco  43878  volioof  44690  fvvolioof  44692  fvvolicof  44694  fourierdlem42  44852  hoi2toco  45310  ovolval2lem  45346  ovolval3  45350  ovolval4lem1  45352  ovolval5lem2  45356  ovnovollem1  45359  ovnovollem2  45360  smfpimbor1lem1  45501  aovfundmoveq  45876  aovpcov0  45885  aovnuoveq  45886  aovvoveq  45887  aov0ov0  45888  aovovn0oveq  45889  aov0nbovbi  45890  aovov0bi  45891  ovn0dmfun  46521  ovn0ssdmfun  46524  plusfreseq  46529  idfusubc0  46626  rhmsubclem2  46939  rhmsubcALTVlem2  46957  lmod1lem2  47123  lmod1lem3  47124  rrx2xpref1o  47358  rrx2plordisom  47363  fvconstr  47476  fvconstrn0  47477  fvconstr2  47478  funcf2lem  47592  indthinc  47626  prsthinc  47628  mndtchom  47664  mndtcco  47665  logb2aval  47763
  Copyright terms: Public domain W3C validator