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 7148
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 11777). This definition is well-defined, although not very meaningful, when classes 𝐴 and/or 𝐵 are proper classes (i.e. are not sets); see ovprc1 7184 and ovprc2 7185. On the other hand, we often find uses for this definition when 𝐹 is a proper class, such as +o in oav 8127. 𝐹 is normally equal to a class of nested ordered pairs of the form defined by df-oprab 7149. (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 7145 . 2 class (𝐴𝐹𝐵)
51, 2cop 4565 . . 3 class 𝐴, 𝐵
65, 3cfv 6349 . 2 class (𝐹‘⟨𝐴, 𝐵⟩)
74, 6wceq 1528 1 wff (𝐴𝐹𝐵) = (𝐹‘⟨𝐴, 𝐵⟩)
Colors of variables: wff setvar class
This definition is referenced by:  oveq  7151  oveq1  7152  oveq2  7153  nfovd  7174  ovex  7178  ovssunirn  7181  0ov  7182  ovprc  7183  csbov123  7187  csbov  7188  elovimad  7193  fnbrovb  7194  f1opr  7199  ffnov  7267  eqfnov  7269  fnov  7271  ovid  7280  ovidig  7281  ov  7283  ovigg  7284  ov6g  7301  ovg  7302  ovres  7303  fovrn  7307  fnrnov  7310  foov  7311  fnovrn  7312  funimassov  7314  ovelimab  7315  ovima0  7316  ovconst2  7317  oprssdm  7318  nssdmovg  7319  ndmovg  7320  elmpocl  7376  1st2val  7708  2nd2val  7709  brovpreldm  7775  bropopvvv  7776  bropfvvvvlem  7777  ovmptss  7779  oprab2co  7783  curry1  7790  curry2  7793  fsplitfpar  7805  offsplitfpar  7806  algrflem  7810  fvproj  7819  mpoxeldm  7868  mpoxopn0yelv  7870  mpoxopxnop0  7872  ovtpos  7898  mpocurryd  7926  seqomlem1  8077  seqomlem4  8080  brwitnlem  8123  cantnfvalf  9117  fseqenlem1  9439  axdc4lem  9866  fpwwe  10057  canthwelem  10061  addpiord  10295  mulpiord  10296  addpqnq  10349  mulpqnq  10352  recmulnq  10375  dmrecnq  10379  cnref1o  12374  ixxssxr  12740  om2uzrdg  13314  uzrdgsuci  13318  seqexw  13375  swrd00  13996  swrd0  14010  pfx00  14026  pfx0  14027  cnrecnv  14514  sadcf  15792  smupf  15817  eucalgval  15916  eucalginv  15918  eucalglt  15919  eucalg  15921  vdwmc  16304  isstruct2  16483  isstruct  16486  setsstruct2  16511  imasaddvallem  16792  imasvscafn  16800  imasvscaval  16801  xpsff1o  16830  xpsaddlem  16836  xpsvsca  16840  xpsle  16842  comffval  16959  comfffval2  16961  comfeq  16966  isoval  17025  brcic  17058  isssc  17080  isfuncd  17125  funcf2  17128  idfu2nd  17137  idfucl  17141  cofucl  17148  resfval2  17153  resf2nd  17155  funcres2b  17157  funcpropd  17160  homaval  17281  homarcl2  17285  arwhoma  17295  coapm  17321  catcco  17351  catcisolem  17356  xpcco  17423  xpcid  17429  xpcpropd  17448  evlfcllem  17461  evlfcl  17462  curf1cl  17468  curf2cl  17471  curfcl  17472  uncf1  17476  uncf2  17477  uncfcurf  17479  diag11  17483  diag12  17484  diag2  17485  curf2ndf  17487  hof2fval  17495  hofcl  17499  hofpropd  17507  yonedalem21  17513  yonedalem22  17518  yonedalem3b  17519  yonedalem3  17520  yonedainv  17521  yonffthlem  17522  joinval  17605  meetval  17619  plusffval  17848  mgm1  17858  sgrp1  17900  mnd1  17942  mnd1id  17943  grpsubfval  18087  grp1  18146  mulgfval  18166  gaid  18369  efgmnvl  18771  efgval2  18781  vrgpinv  18826  frgpuptinv  18828  frgpuplem  18829  frgpup2  18833  frgpup3lem  18834  frgpnabllem1  18924  gsum2dlem1  19021  gsum2dlem2  19022  gsum2d  19023  gsum2d2lem  19024  gsumcom2  19026  gsumxp2  19031  eldprd  19057  dprd2dlem2  19093  dprd2dlem1  19094  dprd2da  19095  srgfcl  19196  ring1  19283  scaffval  19583  ply1frcl  20411  ipffval  20722  mamudi  20942  mamudir  20943  mamuvs1  20944  mamuvs2  20945  matplusgcell  20972  matsubgcell  20973  matvscacell  20975  mat1dimmul  21015  mat1rhmelval  21019  mdetrlin  21141  mdetrsca  21142  pmatcoe1fsupp  21239  iccordt  21752  iscnp2  21777  ptbasfi  22119  txcnpi  22146  txdis1cn  22173  lmcn2  22187  xkococn  22198  cnmpt12f  22204  cnmpt21  22209  cnmpt2t  22211  cnmpt22  22212  cnmpt2k  22226  xkohmeo  22353  flfcnp2  22545  tmdcn2  22627  clssubg  22646  tgphaus  22654  qustgplem  22658  psmetxrge0  22852  imasdsf1olem  22912  xpsdsval  22920  xmeterval  22971  comet  23052  txmetcnp  23086  metustid  23093  metustsym  23094  metustexhalf  23095  blval2  23101  metuel2  23104  nrmmetd  23113  nmfval  23127  isngp3  23136  ngpds  23142  tngnm  23189  qtopbaslem  23296  cnmetdval  23308  remetdval  23326  tgqioo  23337  bndth  23491  htpyco2  23512  phtpyco2  23523  caubl  23840  caublcls  23841  bcthlem1  23856  bcthlem2  23857  bcthlem4  23859  bcthlem5  23860  ovolfioo  23997  ovolficc  23998  ovolficcss  23999  ovolfsval  24000  ovolctb  24020  ovoliunlem2  24033  ovolicc2lem1  24047  ovolicc2lem5  24051  ovolfs2  24101  ioorinv  24106  uniiccdif  24108  uniioovol  24109  uniiccvol  24110  uniioombllem2a  24112  uniioombllem2  24113  uniioombllem3a  24114  uniioombllem3  24115  uniioombllem4  24116  uniioombllem5  24117  uniioombllem6  24118  dyadovol  24123  dyadss  24124  dyaddisjlem  24125  dyadmaxlem  24127  dyadmbl  24130  opnmbllem  24131  itg1addlem4  24229  limccnp2  24419  dvbsss  24429  perfdvf  24430  dvdsmulf1o  25699  fsumdvdsmul  25700  fsumvma  25717  tgjustc1  26189  tgjustc2  26190  tglngne  26264  ltgseg  26310  tgelrnln  26344  opvtxov  26718  opiedgov  26721  edgov  26765  vtxdgop  27180  finsumvtxdg2size  27260  ex-fpar  28169  imsdval  28391  ofresid  30318  ofoprabco  30338  suppovss  30355  fsuppcurry1  30388  fsuppcurry2  30389  xrofsup  30419  fedgmullem2  30926  smatrcl  30961  smatlem  30962  elunirnmbfm  31411  sibfof  31498  oddpwdcv  31513  eulerpartlemgh  31536  cndprobval  31591  cvmlift2lem9  32456  cvmlift2lem10  32457  cvmlift2lem13  32460  cvmliftphtlem  32462  goel  32492  gonafv  32495  sat1el2xp  32524  madeval2  33188  fvtransport  33391  fvray  33500  linedegen  33502  fvline  33503  bj-finsumval0  34456  icoreunrn  34523  relowlpssretop  34528  finxpreclem1  34553  finxpreclem2  34554  finxpreclem3  34557  finxpreclem5  34559  curfv  34754  uncov  34755  curunc  34756  opnmbllem0  34810  mblfinlem1  34811  mblfinlem2  34812  ftc1anc  34857  ftc2nc  34858  opropabco  34882  ismtyhmeolem  34965  heiborlem3  34974  heiborlem4  34975  heiborlem6  34977  heiborlem8  34979  grposnOLD  35043  fvovco  41335  volioof  42153  fvvolioof  42155  fvvolicof  42157  fourierdlem42  42315  hoi2toco  42770  ovolval2lem  42806  ovolval3  42810  ovolval4lem1  42812  ovolval5lem2  42816  ovnovollem1  42819  ovnovollem2  42820  smfpimbor1lem1  42954  aovfundmoveq  43261  aovpcov0  43270  aovnuoveq  43271  aovvoveq  43272  aov0ov0  43273  aovovn0oveq  43274  aov0nbovbi  43275  aovov0bi  43276  ovn0dmfun  43878  ovn0ssdmfun  43881  plusfreseq  43886  idfusubc0  44034  rhmsubclem2  44256  rhmsubcALTVlem2  44274  lmod1lem2  44441  lmod1lem3  44442  rrx2xpref1o  44603  rrx2plordisom  44608  logb2aval  44761
  Copyright terms: Public domain W3C validator