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 6794
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 11360). This definition is well-defined, although not very meaningful, when classes 𝐴 and/or 𝐵 are proper classes (i.e. are not sets); see ovprc1 6827 and ovprc2 6828. On the other hand, we often find uses for this definition when 𝐹 is a proper class, such as +𝑜 in oav 7743. 𝐹 is normally equal to a class of nested ordered pairs of the form defined by df-oprab 6795. (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 6791 . 2 class (𝐴𝐹𝐵)
51, 2cop 4322 . . 3 class 𝐴, 𝐵
65, 3cfv 6029 . 2 class (𝐹‘⟨𝐴, 𝐵⟩)
74, 6wceq 1631 1 wff (𝐴𝐹𝐵) = (𝐹‘⟨𝐴, 𝐵⟩)
Colors of variables: wff setvar class
This definition is referenced by:  oveq  6797  oveq1  6798  oveq2  6799  nfovd  6818  ovex  6821  ovssunirn  6824  0ov  6825  ovprc  6826  csbov123  6830  csbov  6831  elovimad  6836  fnbrovb  6837  fnotovbOLD  6839  ffnov  6909  eqfnov  6911  fnov  6913  ovid  6922  ovidig  6923  ov  6925  ovigg  6926  ov6g  6943  ovg  6944  ovres  6945  fovrn  6949  fnrnov  6952  foov  6953  fnovrn  6954  funimassov  6956  ovelimab  6957  ovima0  6958  ovconst2  6959  oprssdm  6960  nssdmovg  6961  ndmovg  6962  elmpt2cl  7021  1st2val  7341  2nd2val  7342  brovpreldm  7403  bropopvvv  7404  bropfvvvvlem  7405  ovmptss  7407  oprab2co  7411  curry1  7418  curry2  7421  algrflem  7435  mpt2xeldm  7487  mpt2xopn0yelv  7489  mpt2xopxnop0  7491  ovtpos  7517  mpt2curryd  7545  seqomlem1  7696  seqomlem4  7699  brwitnlem  7739  cantnfvalf  8724  fseqenlem1  9045  axdc4lem  9477  fpwwe  9668  canthwelem  9672  addpiord  9906  mulpiord  9907  addpqnq  9960  mulpqnq  9963  recmulnq  9986  dmrecnq  9990  cnref1o  12023  ixxssxr  12385  om2uzrdg  12956  uzrdgsuci  12960  swrd00  13619  swrd0  13636  cnrecnv  14106  sadcf  15376  smupf  15401  eucalgval  15496  eucalginv  15498  eucalglt  15499  eucalg  15501  vdwmc  15882  isstruct2  16067  isstruct  16070  setsstruct2  16096  imasaddvallem  16390  imasvscafn  16398  imasvscaval  16399  xpsff1o  16429  xpsaddlem  16436  xpsvsca  16440  xpsle  16442  comffval  16559  comfffval2  16561  comfeq  16566  isoval  16625  brcic  16658  isssc  16680  isfuncd  16725  funcf2  16728  idfu2nd  16737  idfucl  16741  cofucl  16748  resfval2  16753  resf2nd  16755  funcres2b  16757  funcpropd  16760  homaval  16881  homarcl2  16885  arwhoma  16895  coapm  16921  catcco  16951  catcisolem  16956  xpcco  17024  xpcid  17030  xpcpropd  17049  evlfcllem  17062  evlfcl  17063  curf1cl  17069  curf2cl  17072  curfcl  17073  uncf1  17077  uncf2  17078  uncfcurf  17080  diag11  17084  diag12  17085  diag2  17086  curf2ndf  17088  hof2fval  17096  hofcl  17100  hofpropd  17108  yonedalem21  17114  yonedalem22  17119  yonedalem3b  17120  yonedalem3  17121  yonedainv  17122  yonffthlem  17123  joinval  17206  meetval  17220  plusffval  17448  mgm1  17458  sgrp1  17494  mnd1  17532  mnd1id  17533  grp1  17723  gaid  17932  efgmnvl  18327  efgval2  18337  vrgpinv  18382  frgpuptinv  18384  frgpuplem  18385  frgpup2  18389  frgpup3lem  18390  frgpnabllem1  18476  gsum2dlem1  18569  gsum2dlem2  18570  gsum2d  18571  gsum2d2lem  18572  gsumcom2  18574  eldprd  18604  dprd2dlem2  18640  dprd2dlem1  18641  dprd2da  18642  srgfcl  18716  ring1  18803  scaffval  19084  ply1frcl  19891  ipffval  20203  mamudi  20419  mamudir  20420  mamuvs1  20421  mamuvs2  20422  matplusgcell  20449  matsubgcell  20450  matvscacell  20452  mat1dimmul  20493  mat1rhmelval  20497  mdetrlin  20619  mdetrsca  20620  pmatcoe1fsupp  20719  iccordt  21232  iscnp2  21257  ptbasfi  21598  txcnpi  21625  txdis1cn  21652  lmcn2  21666  xkococn  21677  cnmpt12f  21683  cnmpt21  21688  cnmpt2t  21690  cnmpt22  21691  cnmpt2k  21705  xkohmeo  21832  flfcnp2  22024  tmdcn2  22106  clssubg  22125  tgphaus  22133  qustgplem  22137  psmetxrge0  22331  imasdsf1olem  22391  xpsdsval  22399  xmeterval  22450  comet  22531  txmetcnp  22565  metustid  22572  metustsym  22573  metustexhalf  22574  blval2  22580  metuel2  22583  nrmmetd  22592  nmfval  22606  isngp3  22615  ngpds  22621  tngnm  22668  qtopbaslem  22775  cnmetdval  22787  remetdval  22805  tgqioo  22816  bndth  22970  htpyco2  22991  phtpyco2  23002  caubl  23318  caublcls  23319  bcthlem1  23333  bcthlem2  23334  bcthlem4  23336  bcthlem5  23337  ovolfioo  23448  ovolficc  23449  ovolficcss  23450  ovolfsval  23451  ovolctb  23471  ovoliunlem2  23484  ovolicc2lem1  23498  ovolicc2lem5  23502  ovolfs2  23552  ioorinv  23557  uniiccdif  23559  uniioovol  23560  uniiccvol  23561  uniioombllem2a  23563  uniioombllem2  23564  uniioombllem3a  23565  uniioombllem3  23566  uniioombllem4  23567  uniioombllem5  23568  uniioombllem6  23569  dyadovol  23574  dyadss  23575  dyaddisjlem  23576  dyadmaxlem  23578  dyadmbl  23581  opnmbllem  23582  itg1addlem4  23679  limccnp2  23869  dvbsss  23879  perfdvf  23880  dvdsmulf1o  25134  fsumdvdsmul  25135  fsumvma  25152  tglngne  25659  ltgseg  25705  tgelrnln  25739  opvtxov  26099  opiedgov  26102  edgov  26159  vtxdgop  26594  finsumvtxdg2size  26674  imsdval  27874  ofresid  29777  ofoprabco  29797  xrofsup  29866  smatrcl  30195  smatlem  30196  fvproj  30232  elunirnmbfm  30648  sibfof  30735  oddpwdcv  30750  eulerpartlemgh  30773  cndprobval  30828  cvmlift2lem9  31624  cvmlift2lem10  31625  cvmlift2lem13  31628  cvmliftphtlem  31630  madeval2  32266  fvtransport  32469  fvray  32578  linedegen  32580  fvline  32581  bj-finsumval0  33477  icoreunrn  33537  relowlpssretop  33542  finxpreclem1  33556  finxpreclem2  33557  finxpreclem3  33560  finxpreclem5  33562  curfv  33715  uncov  33716  curunc  33717  opnmbllem0  33771  mblfinlem1  33772  mblfinlem2  33773  ftc1anc  33818  ftc2nc  33819  opropabco  33843  f1opr  33844  ismtyhmeolem  33928  heiborlem3  33937  heiborlem4  33938  heiborlem6  33940  heiborlem8  33942  grposnOLD  34006  fvovco  39894  volioof  40714  fvvolioof  40716  fvvolicof  40718  fourierdlem42  40876  hoi2toco  41334  ovolval2lem  41370  ovolval3  41374  ovolval4lem1  41376  ovolval5lem2  41380  ovnovollem1  41383  ovnovollem2  41384  smfpimbor1lem1  41518  aovfundmoveq  41774  aovpcov0  41783  aovnuoveq  41784  aovvoveq  41785  aov0ov0  41786  aovovn0oveq  41787  aov0nbovbi  41788  aovov0bi  41789  pfx00  41905  pfx0  41906  ovn0dmfun  42285  ovn0ssdmfun  42288  plusfreseq  42293  idfusubc0  42386  rhmsubclem2  42608  rhmsubcALTVlem2  42626  lmod1lem2  42798  lmod1lem3  42799  logb2aval  43029
  Copyright terms: Public domain W3C validator