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 6804
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 11323). This definition is well-defined, although not very meaningful, when classes 𝐴 and/or 𝐵 are proper classes (i.e. are not sets); see ovprc1 6835 and ovprc2 6836. On the other hand, we often find uses for this definition when 𝐹 is a proper class, such as +𝑜 in oav 7748. 𝐹 is normally equal to a class of nested ordered pairs of the form defined by df-oprab 6805. (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 6801 . 2 class (𝐴𝐹𝐵)
51, 2cop 4315 . . 3 class 𝐴, 𝐵
65, 3cfv 6037 . 2 class (𝐹‘⟨𝐴, 𝐵⟩)
74, 6wceq 1620 1 wff (𝐴𝐹𝐵) = (𝐹‘⟨𝐴, 𝐵⟩)
Colors of variables: wff setvar class
This definition is referenced by:  oveq  6807  oveq1  6808  oveq2  6809  nfovd  6826  ovex  6829  ovssunirn  6832  0ov  6833  ovprc  6834  csbov123  6838  csbov  6839  elovimad  6844  fnbrovb  6845  fnotovbOLD  6847  ffnov  6917  eqfnov  6919  fnov  6921  ovid  6930  ovidig  6931  ov  6933  ovigg  6934  ov6g  6951  ovg  6952  ovres  6953  fovrn  6957  fnrnov  6960  foov  6961  fnovrn  6962  funimassov  6964  ovelimab  6965  ovima0  6966  ovconst2  6967  oprssdm  6968  nssdmovg  6969  ndmovg  6970  elmpt2cl  7029  1st2val  7349  2nd2val  7350  brovpreldm  7410  bropopvvv  7411  bropfvvvvlem  7412  ovmptss  7414  oprab2co  7418  curry1  7425  curry2  7428  algrflem  7442  mpt2xeldm  7494  mpt2xopn0yelv  7496  mpt2xopxnop0  7498  ovtpos  7524  mpt2curryd  7552  seqomlem1  7702  seqomlem4  7705  brwitnlem  7744  cantnfvalf  8723  fseqenlem1  9008  axdc4lem  9440  fpwwe  9631  canthwelem  9635  addpiord  9869  mulpiord  9870  addpqnq  9923  mulpqnq  9926  recmulnq  9949  dmrecnq  9953  cnref1o  11991  ixxssxr  12351  om2uzrdg  12920  uzrdgsuci  12924  swrd00  13588  swrd0  13605  cnrecnv  14075  sadcf  15348  smupf  15373  eucalgval  15468  eucalginv  15470  eucalglt  15471  eucalg  15473  vdwmc  15855  isstruct2  16040  isstruct  16043  setsstruct2  16069  imasaddvallem  16362  imasvscafn  16370  imasvscaval  16371  xpsff1o  16401  xpsaddlem  16408  xpsvsca  16412  xpsle  16414  comffval  16531  comfffval2  16533  comfeq  16538  isoval  16597  brcic  16630  isssc  16652  isfuncd  16697  funcf2  16700  idfu2nd  16709  idfucl  16713  cofucl  16720  resfval2  16725  resf2nd  16727  funcres2b  16729  funcpropd  16732  homaval  16853  homarcl2  16857  arwhoma  16867  coapm  16893  catcco  16923  catcisolem  16928  xpcco  16995  xpcid  17001  xpcpropd  17020  evlfcllem  17033  evlfcl  17034  curf1cl  17040  curf2cl  17043  curfcl  17044  uncf1  17048  uncf2  17049  uncfcurf  17051  diag11  17055  diag12  17056  diag2  17057  curf2ndf  17059  hof2fval  17067  hofcl  17071  hofpropd  17079  yonedalem21  17085  yonedalem22  17090  yonedalem3b  17091  yonedalem3  17092  yonedainv  17093  yonffthlem  17094  joinval  17177  meetval  17191  plusffval  17419  mgm1  17429  sgrp1  17465  mnd1  17503  mnd1id  17504  grp1  17694  gaid  17903  efgmnvl  18298  efgval2  18308  vrgpinv  18353  frgpuptinv  18355  frgpuplem  18356  frgpup2  18360  frgpup3lem  18361  frgpnabllem1  18447  gsum2dlem1  18540  gsum2dlem2  18541  gsum2d  18542  gsum2d2lem  18543  gsumcom2  18545  eldprd  18574  dprd2dlem2  18610  dprd2dlem1  18611  dprd2da  18612  srgfcl  18686  ring1  18773  scaffval  19054  ply1frcl  19856  ipffval  20166  mamudi  20382  mamudir  20383  mamuvs1  20384  mamuvs2  20385  matplusgcell  20412  matsubgcell  20413  matvscacell  20415  mat1dimmul  20455  mat1rhmelval  20459  mdetrlin  20581  mdetrsca  20582  pmatcoe1fsupp  20679  iccordt  21191  iscnp2  21216  ptbasfi  21557  txcnpi  21584  txdis1cn  21611  lmcn2  21625  xkococn  21636  cnmpt12f  21642  cnmpt21  21647  cnmpt2t  21649  cnmpt22  21650  cnmpt2k  21664  xkohmeo  21791  flfcnp2  21983  tmdcn2  22065  clssubg  22084  tgphaus  22092  qustgplem  22096  psmetxrge0  22290  imasdsf1olem  22350  xpsdsval  22358  xmeterval  22409  comet  22490  txmetcnp  22524  metustid  22531  metustsym  22532  metustexhalf  22533  blval2  22539  metuel2  22542  nrmmetd  22551  nmfval  22565  isngp3  22574  ngpds  22580  tngnm  22627  qtopbaslem  22734  cnmetdval  22746  remetdval  22764  tgqioo  22775  bndth  22929  htpyco2  22950  phtpyco2  22961  caubl  23277  caublcls  23278  bcthlem1  23292  bcthlem2  23293  bcthlem4  23295  bcthlem5  23296  ovolfioo  23407  ovolficc  23408  ovolficcss  23409  ovolfsval  23410  ovolctb  23429  ovoliunlem2  23442  ovolicc2lem1  23456  ovolicc2lem5  23460  ovolfs2  23510  ioorinv  23515  uniiccdif  23517  uniioovol  23518  uniiccvol  23519  uniioombllem2a  23521  uniioombllem2  23522  uniioombllem3a  23523  uniioombllem3  23524  uniioombllem4  23525  uniioombllem5  23526  uniioombllem6  23527  dyadovol  23532  dyadss  23533  dyaddisjlem  23534  dyadmaxlem  23536  dyadmbl  23539  opnmbllem  23540  itg1addlem4  23636  limccnp2  23826  dvbsss  23836  perfdvf  23837  dvdsmulf1o  25090  fsumdvdsmul  25091  fsumvma  25108  tglngne  25615  ltgseg  25661  tgelrnln  25695  opvtxov  26055  opiedgov  26058  edgov  26115  vtxdgop  26547  finsumvtxdg2size  26627  imsdval  27821  ofresid  29724  ofoprabco  29744  xrofsup  29813  smatrcl  30142  smatlem  30143  fvproj  30179  elunirnmbfm  30595  sibfof  30682  oddpwdcv  30697  eulerpartlemgh  30720  cndprobval  30775  cvmlift2lem9  31571  cvmlift2lem10  31572  cvmlift2lem13  31575  cvmliftphtlem  31577  madeval2  32213  fvtransport  32416  fvray  32525  linedegen  32527  fvline  32528  bj-finsumval0  33429  icoreunrn  33489  relowlpssretop  33494  finxpreclem1  33508  finxpreclem2  33509  finxpreclem3  33512  finxpreclem5  33514  curfv  33671  uncov  33672  curunc  33673  opnmbllem0  33727  mblfinlem1  33728  mblfinlem2  33729  ftc1anc  33775  ftc2nc  33776  opropabco  33800  f1opr  33801  ismtyhmeolem  33885  heiborlem3  33894  heiborlem4  33895  heiborlem6  33897  heiborlem8  33899  grposnOLD  33963  fvovco  39849  volioof  40676  fvvolioof  40678  fvvolicof  40680  fourierdlem42  40838  hoi2toco  41296  ovolval2lem  41332  ovolval3  41336  ovolval4lem1  41338  ovolval5lem2  41342  ovnovollem1  41345  ovnovollem2  41346  smfpimbor1lem1  41480  aovfundmoveq  41736  aovpcov0  41745  aovnuoveq  41746  aovvoveq  41747  aov0ov0  41748  aovovn0oveq  41749  aov0nbovbi  41750  aovov0bi  41751  pfx00  41863  pfx0  41864  ovn0dmfun  42243  ovn0ssdmfun  42246  plusfreseq  42251  idfusubc0  42344  rhmsubclem2  42566  rhmsubcALTVlem2  42584  lmod1lem2  42756  lmod1lem3  42757  logb2aval  42987
  Copyright terms: Public domain W3C validator