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

Definition df-ov 6552
 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 11037). This definition is well-defined, although not very meaningful, when classes 𝐴 and/or 𝐵 are proper classes (i.e. are not sets); see ovprc1 6582 and ovprc2 6583. On the other hand, we often find uses for this definition when 𝐹 is a proper class, such as +𝑜 in oav 7478. 𝐹 is normally equal to a class of nested ordered pairs of the form defined by df-oprab 6553. (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 6549 . 2 class (𝐴𝐹𝐵)
51, 2cop 4131 . . 3 class 𝐴, 𝐵
65, 3cfv 5804 . 2 class (𝐹‘⟨𝐴, 𝐵⟩)
74, 6wceq 1475 1 wff (𝐴𝐹𝐵) = (𝐹‘⟨𝐴, 𝐵⟩)
 Colors of variables: wff setvar class This definition is referenced by:  oveq  6555  oveq1  6556  oveq2  6557  nfovd  6574  ovex  6577  ovssunirn  6579  0ov  6580  ovprc  6581  csbov123  6585  csbov  6586  elovimad  6591  fnotovb  6592  ffnov  6662  eqfnov  6664  fnov  6666  ovid  6675  ovidig  6676  ov  6678  ovigg  6679  ov6g  6696  ovg  6697  ovres  6698  fovrn  6702  fnrnov  6705  foov  6706  fnovrn  6707  funimassov  6709  ovelimab  6710  ovima0  6711  ovconst2  6712  oprssdm  6713  nssdmovg  6714  ndmovg  6715  elmpt2cl  6774  1st2val  7085  2nd2val  7086  brovpreldm  7141  bropopvvv  7142  bropfvvvvlem  7143  ovmptss  7145  oprab2co  7149  curry1  7156  curry2  7159  algrflem  7173  mpt2xeldm  7224  mpt2xopn0yelv  7226  mpt2xopxnop0  7228  ovtpos  7254  mpt2curryd  7282  seqomlem1  7432  seqomlem4  7435  brwitnlem  7474  cantnfvalf  8445  fseqenlem1  8730  axdc4lem  9160  fpwwe  9347  canthwelem  9351  addpiord  9585  mulpiord  9586  addpqnq  9639  mulpqnq  9642  recmulnq  9665  dmrecnq  9669  cnref1o  11703  ixxssxr  12058  om2uzrdg  12617  uzrdgsuci  12621  swrd00  13270  swrd0  13286  cnrecnv  13753  sadcf  15013  smupf  15038  eucalgval  15133  eucalginv  15135  eucalglt  15136  eucalg  15138  vdwmc  15520  isstruct2  15704  isstruct  15705  imasaddvallem  16012  imasvscafn  16020  imasvscaval  16021  xpsff1o  16051  xpsaddlem  16058  xpsvsca  16062  xpsle  16064  comffval  16182  comfffval2  16184  comfeq  16189  isoval  16248  brcic  16281  isssc  16303  isfuncd  16348  funcf2  16351  idfu2nd  16360  idfucl  16364  cofucl  16371  resfval2  16376  resf2nd  16378  funcres2b  16380  funcpropd  16383  homaval  16504  homarcl2  16508  arwhoma  16518  coapm  16544  catcco  16574  catcisolem  16579  xpcco  16646  xpcid  16652  xpcpropd  16671  evlfcllem  16684  evlfcl  16685  curf1cl  16691  curf2cl  16694  curfcl  16695  uncf1  16699  uncf2  16700  uncfcurf  16702  diag11  16706  diag12  16707  diag2  16708  curf2ndf  16710  hof2fval  16718  hofcl  16722  hofpropd  16730  yonedalem21  16736  yonedalem22  16741  yonedalem3b  16742  yonedalem3  16743  yonedainv  16744  yonffthlem  16745  joinval  16828  meetval  16842  plusffval  17070  mgm1  17080  sgrp1  17116  mnd1  17154  mnd1id  17155  grp1  17345  gaid  17555  efgmnvl  17950  efgval2  17960  vrgpinv  18005  frgpuptinv  18007  frgpuplem  18008  frgpup2  18012  frgpup3lem  18013  frgpnabllem1  18099  gsum2dlem1  18192  gsum2dlem2  18193  gsum2d  18194  gsum2d2lem  18195  gsumcom2  18197  eldprd  18226  dprd2dlem2  18262  dprd2dlem1  18263  dprd2da  18264  srgfcl  18338  ring1  18425  scaffval  18704  ply1frcl  19504  ipffval  19812  mamudi  20028  mamudir  20029  mamuvs1  20030  mamuvs2  20031  matplusgcell  20058  matsubgcell  20059  matvscacell  20061  mat1dimmul  20101  mat1rhmelval  20105  mdetrlin  20227  mdetrsca  20228  pmatcoe1fsupp  20325  iccordt  20828  iscnp2  20853  ptbasfi  21194  txcnpi  21221  txdis1cn  21248  lmcn2  21262  xkococn  21273  cnmpt12f  21279  cnmpt21  21284  cnmpt2t  21286  cnmpt22  21287  cnmpt2k  21301  xkohmeo  21428  flfcnp2  21621  tmdcn2  21703  clssubg  21722  tgphaus  21730  qustgplem  21734  psmetxrge0  21928  imasdsf1olem  21988  xpsdsval  21996  xmeterval  22047  comet  22128  txmetcnp  22162  metustid  22169  metustsym  22170  metustexhalf  22171  blval2  22177  metuel2  22180  nrmmetd  22189  nmfval  22203  isngp3  22212  ngpds  22218  tngnm  22265  qtopbaslem  22372  cnmetdval  22384  remetdval  22400  tgqioo  22411  bndth  22565  htpyco2  22586  phtpyco2  22597  caubl  22914  caublcls  22915  bcthlem1  22929  bcthlem2  22930  bcthlem4  22932  bcthlem5  22933  ovolfioo  23043  ovolficc  23044  ovolficcss  23045  ovolfsval  23046  ovolctb  23065  ovoliunlem2  23078  ovolicc2lem1  23092  ovolicc2lem5  23096  ovolfs2  23145  ioorinv  23150  uniiccdif  23152  uniioovol  23153  uniiccvol  23154  uniioombllem2a  23156  uniioombllem2  23157  uniioombllem3a  23158  uniioombllem3  23159  uniioombllem4  23160  uniioombllem5  23161  uniioombllem6  23162  dyadovol  23167  dyadss  23168  dyaddisjlem  23169  dyadmaxlem  23171  dyadmbl  23174  opnmbllem  23175  itg1addlem4  23272  limccnp2  23462  dvbsss  23472  perfdvf  23473  dvdsmulf1o  24720  fsumdvdsmul  24721  fsumvma  24738  tglngne  25245  ltgseg  25291  tgelrnln  25325  opvtxov  25682  opiedgov  25685  edgaov  25796  edgov  25870  usgraexmplvtx  25931  usgraexmplcvtx  25934  usgraexmplcedg  25935  2wlkonot3v  26402  2spthonot3v  26403  isrgrac  26461  imsdval  26925  ofresid  28824  ofoprabco  28847  xrofsup  28923  smatrcl  29190  smatlem  29191  fvproj  29227  elunirnmbfm  29642  sibfof  29729  oddpwdcv  29744  eulerpartlemgh  29767  cndprobval  29822  cvmlift2lem9  30547  cvmlift2lem10  30548  cvmlift2lem13  30551  cvmliftphtlem  30553  fvtransport  31309  fvray  31418  linedegen  31420  fvline  31421  bj-finsumval0  32324  icoreunrn  32383  relowlpssretop  32388  finxpreclem1  32402  finxpreclem2  32403  finxpreclem3  32406  finxpreclem5  32408  curfv  32559  uncov  32560  curunc  32561  opnmbllem0  32615  mblfinlem1  32616  mblfinlem2  32617  ftc1anc  32663  ftc2nc  32664  opropabco  32688  f1opr  32689  ismtyhmeolem  32773  heiborlem3  32782  heiborlem4  32783  heiborlem6  32785  heiborlem8  32787  grposnOLD  32851  fvovco  38376  volioof  38880  fvvolioof  38882  fvvolicof  38884  fourierdlem42  39042  hoi2toco  39497  ovolval2lem  39533  ovolval3  39537  ovolval4lem1  39539  ovolval5lem2  39543  ovnovollem1  39546  ovnovollem2  39547  smfpimbor1lem1  39683  aovfundmoveq  39910  aovpcov0  39919  aovnuoveq  39920  aovvoveq  39921  aov0ov0  39922  aovovn0oveq  39923  aov0nbovbi  39924  aovov0bi  39925  pfx00  40247  pfx0  40248  ovn0dmfun  41554  ovn0ssdmfun  41557  plusfreseq  41562  idfusubc0  41655  rhmsubclem2  41879  rhmsubcALTVlem2  41898  lmod1lem2  42071  lmod1lem3  42072  logb2aval  42314
 Copyright terms: Public domain W3C validator