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 6638
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 11145). This definition is well-defined, although not very meaningful, when classes 𝐴 and/or 𝐵 are proper classes (i.e. are not sets); see ovprc1 6669 and ovprc2 6670. On the other hand, we often find uses for this definition when 𝐹 is a proper class, such as +𝑜 in oav 7576. 𝐹 is normally equal to a class of nested ordered pairs of the form defined by df-oprab 6639. (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 6635 . 2 class (𝐴𝐹𝐵)
51, 2cop 4174 . . 3 class 𝐴, 𝐵
65, 3cfv 5876 . 2 class (𝐹‘⟨𝐴, 𝐵⟩)
74, 6wceq 1481 1 wff (𝐴𝐹𝐵) = (𝐹‘⟨𝐴, 𝐵⟩)
Colors of variables: wff setvar class
This definition is referenced by:  oveq  6641  oveq1  6642  oveq2  6643  nfovd  6660  ovex  6663  ovssunirn  6666  0ov  6667  ovprc  6668  csbov123  6672  csbov  6673  elovimad  6678  fnotovb  6679  ffnov  6749  eqfnov  6751  fnov  6753  ovid  6762  ovidig  6763  ov  6765  ovigg  6766  ov6g  6783  ovg  6784  ovres  6785  fovrn  6789  fnrnov  6792  foov  6793  fnovrn  6794  funimassov  6796  ovelimab  6797  ovima0  6798  ovconst2  6799  oprssdm  6800  nssdmovg  6801  ndmovg  6802  elmpt2cl  6861  1st2val  7179  2nd2val  7180  brovpreldm  7239  bropopvvv  7240  bropfvvvvlem  7241  ovmptss  7243  oprab2co  7247  curry1  7254  curry2  7257  algrflem  7271  mpt2xeldm  7322  mpt2xopn0yelv  7324  mpt2xopxnop0  7326  ovtpos  7352  mpt2curryd  7380  seqomlem1  7530  seqomlem4  7533  brwitnlem  7572  cantnfvalf  8547  fseqenlem1  8832  axdc4lem  9262  fpwwe  9453  canthwelem  9457  addpiord  9691  mulpiord  9692  addpqnq  9745  mulpqnq  9748  recmulnq  9771  dmrecnq  9775  cnref1o  11812  ixxssxr  12172  om2uzrdg  12738  uzrdgsuci  12742  swrd00  13400  swrd0  13416  cnrecnv  13886  sadcf  15156  smupf  15181  eucalgval  15276  eucalginv  15278  eucalglt  15279  eucalg  15281  vdwmc  15663  isstruct2  15848  isstruct  15851  setsstruct2  15877  imasaddvallem  16170  imasvscafn  16178  imasvscaval  16179  xpsff1o  16209  xpsaddlem  16216  xpsvsca  16220  xpsle  16222  comffval  16340  comfffval2  16342  comfeq  16347  isoval  16406  brcic  16439  isssc  16461  isfuncd  16506  funcf2  16509  idfu2nd  16518  idfucl  16522  cofucl  16529  resfval2  16534  resf2nd  16536  funcres2b  16538  funcpropd  16541  homaval  16662  homarcl2  16666  arwhoma  16676  coapm  16702  catcco  16732  catcisolem  16737  xpcco  16804  xpcid  16810  xpcpropd  16829  evlfcllem  16842  evlfcl  16843  curf1cl  16849  curf2cl  16852  curfcl  16853  uncf1  16857  uncf2  16858  uncfcurf  16860  diag11  16864  diag12  16865  diag2  16866  curf2ndf  16868  hof2fval  16876  hofcl  16880  hofpropd  16888  yonedalem21  16894  yonedalem22  16899  yonedalem3b  16900  yonedalem3  16901  yonedainv  16902  yonffthlem  16903  joinval  16986  meetval  17000  plusffval  17228  mgm1  17238  sgrp1  17274  mnd1  17312  mnd1id  17313  grp1  17503  gaid  17713  efgmnvl  18108  efgval2  18118  vrgpinv  18163  frgpuptinv  18165  frgpuplem  18166  frgpup2  18170  frgpup3lem  18171  frgpnabllem1  18257  gsum2dlem1  18350  gsum2dlem2  18351  gsum2d  18352  gsum2d2lem  18353  gsumcom2  18355  eldprd  18384  dprd2dlem2  18420  dprd2dlem1  18421  dprd2da  18422  srgfcl  18496  ring1  18583  scaffval  18862  ply1frcl  19664  ipffval  19974  mamudi  20190  mamudir  20191  mamuvs1  20192  mamuvs2  20193  matplusgcell  20220  matsubgcell  20221  matvscacell  20223  mat1dimmul  20263  mat1rhmelval  20267  mdetrlin  20389  mdetrsca  20390  pmatcoe1fsupp  20487  iccordt  20999  iscnp2  21024  ptbasfi  21365  txcnpi  21392  txdis1cn  21419  lmcn2  21433  xkococn  21444  cnmpt12f  21450  cnmpt21  21455  cnmpt2t  21457  cnmpt22  21458  cnmpt2k  21472  xkohmeo  21599  flfcnp2  21792  tmdcn2  21874  clssubg  21893  tgphaus  21901  qustgplem  21905  psmetxrge0  22099  imasdsf1olem  22159  xpsdsval  22167  xmeterval  22218  comet  22299  txmetcnp  22333  metustid  22340  metustsym  22341  metustexhalf  22342  blval2  22348  metuel2  22351  nrmmetd  22360  nmfval  22374  isngp3  22383  ngpds  22389  tngnm  22436  qtopbaslem  22543  cnmetdval  22555  remetdval  22573  tgqioo  22584  bndth  22738  htpyco2  22759  phtpyco2  22770  caubl  23087  caublcls  23088  bcthlem1  23102  bcthlem2  23103  bcthlem4  23105  bcthlem5  23106  ovolfioo  23217  ovolficc  23218  ovolficcss  23219  ovolfsval  23220  ovolctb  23239  ovoliunlem2  23252  ovolicc2lem1  23266  ovolicc2lem5  23270  ovolfs2  23320  ioorinv  23325  uniiccdif  23327  uniioovol  23328  uniiccvol  23329  uniioombllem2a  23331  uniioombllem2  23332  uniioombllem3a  23333  uniioombllem3  23334  uniioombllem4  23335  uniioombllem5  23336  uniioombllem6  23337  dyadovol  23342  dyadss  23343  dyaddisjlem  23344  dyadmaxlem  23346  dyadmbl  23349  opnmbllem  23350  itg1addlem4  23447  limccnp2  23637  dvbsss  23647  perfdvf  23648  dvdsmulf1o  24901  fsumdvdsmul  24902  fsumvma  24919  tglngne  25426  ltgseg  25472  tgelrnln  25506  opvtxov  25866  opiedgov  25869  edgov  25926  vtxdgop  26347  finsumvtxdg2size  26427  imsdval  27511  ofresid  29417  ofoprabco  29438  xrofsup  29507  smatrcl  29836  smatlem  29837  fvproj  29873  elunirnmbfm  30289  sibfof  30376  oddpwdcv  30391  eulerpartlemgh  30414  cndprobval  30469  cvmlift2lem9  31267  cvmlift2lem10  31268  cvmlift2lem13  31271  cvmliftphtlem  31273  madeval2  31910  fvtransport  32114  fvray  32223  linedegen  32225  fvline  32226  bj-finsumval0  33118  icoreunrn  33178  relowlpssretop  33183  finxpreclem1  33197  finxpreclem2  33198  finxpreclem3  33201  finxpreclem5  33203  curfv  33360  uncov  33361  curunc  33362  opnmbllem0  33416  mblfinlem1  33417  mblfinlem2  33418  ftc1anc  33464  ftc2nc  33465  opropabco  33489  f1opr  33490  ismtyhmeolem  33574  heiborlem3  33583  heiborlem4  33584  heiborlem6  33586  heiborlem8  33588  grposnOLD  33652  fvovco  39197  volioof  39967  fvvolioof  39969  fvvolicof  39971  fourierdlem42  40129  hoi2toco  40584  ovolval2lem  40620  ovolval3  40624  ovolval4lem1  40626  ovolval5lem2  40630  ovnovollem1  40633  ovnovollem2  40634  smfpimbor1lem1  40768  aovfundmoveq  41024  aovpcov0  41033  aovnuoveq  41034  aovvoveq  41035  aov0ov0  41036  aovovn0oveq  41037  aov0nbovbi  41038  aovov0bi  41039  pfx00  41149  pfx0  41150  ovn0dmfun  41529  ovn0ssdmfun  41532  plusfreseq  41537  idfusubc0  41630  rhmsubclem2  41852  rhmsubcALTVlem2  41870  lmod1lem2  42042  lmod1lem3  42043  logb2aval  42270
  Copyright terms: Public domain W3C validator