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 7433
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 12414). This definition is well-defined, although not very meaningful, when classes 𝐴 and/or 𝐵 are proper classes (i.e. are not sets); see ovprc1 7469 and ovprc2 7470. On the other hand, we often find uses for this definition when 𝐹 is a proper class, such as +o in oav 8547. 𝐹 is normally equal to a class of nested ordered pairs of the form defined by df-oprab 7434. (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 7430 . 2 class (𝐴𝐹𝐵)
51, 2cop 4636 . . 3 class 𝐴, 𝐵
65, 3cfv 6562 . 2 class (𝐹‘⟨𝐴, 𝐵⟩)
74, 6wceq 1536 1 wff (𝐴𝐹𝐵) = (𝐹‘⟨𝐴, 𝐵⟩)
Colors of variables: wff setvar class
This definition is referenced by:  oveq  7436  oveq1  7437  oveq2  7438  nfovd  7459  ovex  7463  ovssunirn  7466  0ov  7467  ovprc  7468  csbov123  7474  csbov  7475  elovimad  7480  fnbrovb  7481  f1opr  7488  ffnov  7558  eqfnov  7561  fnov  7563  ovid  7573  ovidig  7574  ov  7576  ovigg  7577  fvmpopr2d  7594  ov6g  7596  ovg  7597  ovres  7598  fovcdm  7602  fnrnov  7605  foov  7606  fnovrn  7607  funimassov  7609  ovelimab  7610  ovima0  7611  ovconst2  7612  oprssdm  7613  nssdmovg  7614  ndmovg  7615  elmpocl  7673  1st2val  8040  2nd2val  8041  brovpreldm  8112  bropopvvv  8113  bropfvvvvlem  8114  ovmptss  8116  oprab2co  8120  curry1  8127  curry2  8130  fsplitfpar  8141  offsplitfpar  8142  opco1  8146  opco2  8147  fvproj  8157  mpoxeldm  8234  mpoxopn0yelv  8236  mpoxopxnop0  8238  ovtpos  8264  mpocurryd  8292  seqomlem1  8488  seqomlem4  8491  brwitnlem  8543  on2recsov  8704  naddf  8717  cantnfvalf  9702  fseqenlem1  10061  axdc4lem  10492  fpwwe  10683  canthwelem  10687  addpiord  10921  mulpiord  10922  addpqnq  10975  mulpqnq  10978  recmulnq  11001  dmrecnq  11005  cnref1o  13024  ixxssxr  13395  om2uzrdg  13993  uzrdgsuci  13997  seqexw  14054  swrd00  14678  swrd0  14692  pfx00  14708  pfx0  14709  cnrecnv  15200  sadcf  16486  smupf  16511  eucalgval  16615  eucalginv  16617  eucalglt  16618  eucalg  16620  vdwmc  17011  isstruct2  17182  isstruct  17185  setsstruct2  17207  imasaddvallem  17575  imasvscafn  17583  imasvscaval  17584  xpsff1o  17613  xpsaddlem  17619  xpsvsca  17623  xpsle  17625  comffval  17743  comfffval2  17745  comfeq  17750  isoval  17812  brcic  17845  isssc  17867  isfuncd  17915  funcf2  17918  idfu2nd  17927  idfucl  17931  cofucl  17938  resfval2  17943  resf2nd  17945  funcres2b  17947  idfusubc0  17949  funcpropd  17953  homaval  18084  homarcl2  18088  arwhoma  18098  coapm  18124  catcco  18158  catcisolem  18163  xpcco  18238  xpcid  18244  xpcpropd  18264  evlfcllem  18277  evlfcl  18278  curf1cl  18284  curf2cl  18287  curfcl  18288  uncf1  18292  uncf2  18293  uncfcurf  18295  diag11  18299  diag12  18300  diag2  18301  curf2ndf  18303  hof2fval  18311  hofcl  18315  hofpropd  18323  yonedalem21  18329  yonedalem22  18334  yonedalem3b  18335  yonedalem3  18336  yonedainv  18337  yonffthlem  18338  joinval  18434  meetval  18448  plusffval  18671  mgm1  18683  sgrp1  18754  mnd1  18804  mnd1id  18805  grpsubfval  19013  grp1  19077  mulgfval  19099  gaid  19329  efgmnvl  19746  efgval2  19756  vrgpinv  19801  frgpuptinv  19803  frgpuplem  19804  frgpup2  19808  frgpup3lem  19809  frgpnabllem1  19905  gsum2dlem1  20002  gsum2dlem2  20003  gsum2d  20004  gsum2d2lem  20005  gsumcom2  20007  gsumxp2  20012  eldprd  20038  dprd2dlem2  20074  dprd2dlem1  20075  dprd2da  20076  srgfcl  20213  ring1  20323  rhmsubclem2  20702  scaffval  20894  ipffval  21683  ply1frcl  22337  mamudi  22422  mamudir  22423  mamuvs1  22424  mamuvs2  22425  matplusgcell  22454  matsubgcell  22455  matvscacell  22457  mat1dimmul  22497  mat1rhmelval  22501  mdetrlin  22623  mdetrsca  22624  pmatcoe1fsupp  22722  iccordt  23237  iscnp2  23262  ptbasfi  23604  txcnpi  23631  txdis1cn  23658  lmcn2  23672  xkococn  23683  cnmpt12f  23689  cnmpt21  23694  cnmpt2t  23696  cnmpt22  23697  cnmpt2k  23711  xkohmeo  23838  flfcnp2  24030  tmdcn2  24112  clssubg  24132  tgphaus  24140  qustgplem  24144  psmetxrge0  24338  imasdsf1olem  24398  xpsdsval  24406  xmeterval  24457  comet  24541  txmetcnp  24575  metustid  24582  metustsym  24583  metustexhalf  24584  blval2  24590  metuel2  24593  nrmmetd  24602  nmfval  24616  isngp3  24626  ngpds  24632  tngnm  24687  qtopbaslem  24794  cnmetdval  24806  remetdval  24824  tgqioo  24835  mpomulcn  24904  bndth  25003  htpyco2  25024  phtpyco2  25035  caubl  25355  caublcls  25356  bcthlem1  25371  bcthlem2  25372  bcthlem4  25374  bcthlem5  25375  ovolfioo  25515  ovolficc  25516  ovolficcss  25517  ovolfsval  25518  ovolctb  25538  ovoliunlem2  25551  ovolicc2lem1  25565  ovolicc2lem5  25569  ovolfs2  25619  ioorinv  25624  uniiccdif  25626  uniioovol  25627  uniiccvol  25628  uniioombllem2a  25630  uniioombllem2  25631  uniioombllem3a  25632  uniioombllem3  25633  uniioombllem4  25634  uniioombllem5  25635  uniioombllem6  25636  dyadovol  25641  dyadss  25642  dyaddisjlem  25643  dyadmaxlem  25645  dyadmbl  25648  opnmbllem  25649  itg1addlem4  25747  itg1addlem4OLD  25748  limccnp2  25941  dvbsss  25951  perfdvf  25952  mpodvdsmulf1o  27251  fsumdvdsmul  27252  dvdsmulf1o  27253  fsumdvdsmulOLD  27254  fsumvma  27271  madeval2  27906  scutfo  27956  norec2ov  28004  addsval  28009  addsf  28029  addsfo  28030  subsfo  28109  mulsval  28149  om2noseqrdg  28324  noseqrdgsuc  28328  tgjustc1  28497  tgjustc2  28498  tglngne  28572  ltgseg  28618  tgelrnln  28652  opvtxov  29036  opiedgov  29039  edgov  29083  vtxdgop  29502  finsumvtxdg2size  29582  ex-fpar  30490  imsdval  30714  ofresid  32658  ofoprabco  32680  suppovss  32695  fsuppcurry1  32742  fsuppcurry2  32743  xrofsup  32777  gsumpart  33042  elrgspnlem2  33232  fedgmullem2  33657  smatrcl  33756  smatlem  33757  elunirnmbfm  34232  sibfof  34321  oddpwdcv  34336  eulerpartlemgh  34359  cndprobval  34414  cvmlift2lem9  35295  cvmlift2lem10  35296  cvmlift2lem13  35299  cvmliftphtlem  35301  goel  35331  gonafv  35334  sat1el2xp  35363  fvtransport  36013  fvray  36122  linedegen  36124  fvline  36125  bj-finsumval0  37267  icoreunrn  37341  relowlpssretop  37346  finxpreclem1  37371  finxpreclem2  37372  finxpreclem3  37375  finxpreclem5  37377  curfv  37586  uncov  37587  curunc  37588  opnmbllem0  37642  mblfinlem1  37643  mblfinlem2  37644  ftc1anc  37687  ftc2nc  37688  opropabco  37710  ismtyhmeolem  37790  heiborlem3  37799  heiborlem4  37800  heiborlem6  37802  heiborlem8  37804  grposnOLD  37868  fvovco  45135  volioof  45942  fvvolioof  45944  fvvolicof  45946  fourierdlem42  46104  hoi2toco  46562  ovolval2lem  46598  ovolval3  46602  ovolval4lem1  46604  ovolval5lem2  46608  ovnovollem1  46611  ovnovollem2  46612  smfpimbor1lem1  46753  aovfundmoveq  47130  aovpcov0  47139  aovnuoveq  47140  aovvoveq  47141  aov0ov0  47142  aovovn0oveq  47143  aov0nbovbi  47144  aovov0bi  47145  ovn0dmfun  47999  ovn0ssdmfun  48002  plusfreseq  48007  rhmsubcALTVlem2  48125  lmod1lem2  48333  lmod1lem3  48334  rrx2xpref1o  48567  rrx2plordisom  48572  fvconstr  48685  fvconstrn0  48686  fvconstr2  48687  funcf2lem  48810  indthinc  48852  prsthinc  48854  mndtchom  48892  mndtcco  48893  logb2aval  48994
  Copyright terms: Public domain W3C validator