MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-ov Structured version   Unicode version

Definition df-ov 6284
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  F and its arguments  A and  B- will be useful for proving meaningful theorems. For example, if class  F is the operation  + and arguments  A and  B are  3 and  2, the expression  ( 3  +  2 ) can be proved to equal  5 (see 3p2e5 10675). This definition is well-defined, although not very meaningful, when classes  A and/or  B are proper classes (i.e. are not sets); see ovprc1 6312 and ovprc2 6313. On the other hand, we often find uses for this definition when  F is a proper class, such as  +o in oav 7163.  F is normally equal to a class of nested ordered pairs of the form defined by df-oprab 6285. (Contributed by NM, 28-Feb-1995.)
Assertion
Ref Expression
df-ov  |-  ( A F B )  =  ( F `  <. A ,  B >. )

Detailed syntax breakdown of Definition df-ov
StepHypRef Expression
1 cA . . 3  class  A
2 cB . . 3  class  B
3 cF . . 3  class  F
41, 2, 3co 6281 . 2  class  ( A F B )
51, 2cop 4020 . . 3  class  <. A ,  B >.
65, 3cfv 5578 . 2  class  ( F `
 <. A ,  B >. )
74, 6wceq 1383 1  wff  ( A F B )  =  ( F `  <. A ,  B >. )
Colors of variables: wff setvar class
This definition is referenced by:  oveq  6287  oveq1  6288  oveq2  6289  nfovd  6306  ovex  6309  ovssunirn  6310  ovprc  6311  csbov123  6315  csbov  6316  elovimad  6322  fnotovb  6323  ffnov  6391  eqfnov  6393  fnov  6395  ovid  6404  ovidig  6405  ov  6407  ovigg  6408  ov6g  6425  ovg  6426  ovres  6427  fovrn  6430  fnrnov  6433  foov  6434  fnovrn  6435  funimassov  6437  ovelimab  6438  ovima0  6439  ovconst2  6440  oprssdm  6441  nssdmovg  6442  ndmovg  6443  elmpt2cl  6502  1st2val  6811  2nd2val  6812  bropopvvv  6865  ovmptss  6866  oprab2co  6870  curry1  6877  curry2  6880  algrflem  6894  mpt2xopn0yelv  6943  mpt2xopxnop0  6945  ovtpos  6972  mpt2curryd  7000  seqomlem1  7117  seqomlem4  7120  brwitnlem  7159  cantnfvalf  8087  fseqenlem1  8408  axdc4lem  8838  fpwwe  9027  canthwelem  9031  addpiord  9265  mulpiord  9266  addpqnq  9319  mulpqnq  9322  recmulnq  9345  dmrecnq  9349  cnref1o  11226  ixxssxr  11552  om2uzrdg  12049  uzrdgsuci  12053  swrd00  12627  swrd0  12640  cnrecnv  12980  sadcf  14085  smupf  14110  eucalgval  14193  eucalginv  14195  eucalglt  14196  eucalg  14198  vdwmc  14478  isstruct2  14623  isstruct  14624  imasaddvallem  14908  imasvscafn  14916  imasvscaval  14917  xpsff1o  14947  xpsaddlem  14954  xpsvsca  14958  xpsle  14960  comffval  15076  comfffval2  15078  comfeq  15083  isoval  15141  isssc  15171  isfuncd  15213  funcf2  15216  idfu2nd  15225  idfucl  15229  cofucl  15236  resfval2  15241  resf2nd  15243  funcres2b  15245  funcpropd  15248  homarcl  15334  homaval  15337  homarcl2  15341  arwhoma  15351  coapm  15377  catcco  15407  catcisolem  15412  xpcco  15431  xpcid  15437  xpcpropd  15456  evlfcllem  15469  evlfcl  15470  curf1cl  15476  curf2cl  15479  curfcl  15480  uncf1  15484  uncf2  15485  uncfcurf  15487  diag11  15491  diag12  15492  diag2  15493  curf2ndf  15495  hof2fval  15503  hofcl  15507  hofpropd  15515  yonedalem21  15521  yonedalem22  15526  yonedalem3b  15527  yonedalem3  15528  yonedainv  15529  yonffthlem  15530  joinval  15614  meetval  15628  plusffval  15856  mgm1  15863  sgrp1  15897  mnd1  15940  mnd1OLD  15941  mnd1id  15942  grp1  16121  gaid  16316  oppglsm  16641  efgmnvl  16711  efgval2  16721  vrgpinv  16766  frgpuptinv  16768  frgpuplem  16769  frgpup2  16773  frgpup3lem  16774  frgpnabllem1  16856  gsum2dlem1  16976  gsum2dlem2  16977  gsum2d  16978  gsum2dOLD  16979  gsum2d2lem  16980  gsumcom2  16982  eldprd  17014  eldprdOLD  17016  dprd2dlem2  17068  dprd2dlem1  17069  dprd2da  17070  ring1  17227  scaffval  17509  ply1frcl  18334  ipffval  18661  mamudi  18883  mamudir  18884  mamuvs1  18885  mamuvs2  18886  matplusgcell  18913  matsubgcell  18914  matvscacell  18916  mat1dimmul  18956  mat1rhmelval  18960  mdetrlin  19082  mdetrsca  19083  pmatcoe1fsupp  19180  iccordt  19693  iscnp2  19718  ptbasfi  20060  txcnpi  20087  txdis1cn  20114  lmcn2  20128  xkococn  20139  cnmpt12f  20145  cnmpt21  20150  cnmpt2t  20152  cnmpt22  20153  cnmpt2k  20167  xkohmeo  20294  flfcnp2  20486  tmdcn2  20566  clssubg  20585  tgphaus  20593  qustgplem  20597  psmetxrge0  20795  imasdsf1olem  20854  xpsdsval  20862  xmeterval  20913  comet  20994  txmetcnp  21028  metustidOLD  21040  metustid  21041  metustsymOLD  21042  metustsym  21043  metustexhalfOLD  21044  metustexhalf  21045  blval2  21056  metuel2  21060  nrmmetd  21073  nmfval  21087  isngp3  21096  ngpds  21101  tngnm  21143  qtopbaslem  21243  cnmetdval  21256  remetdval  21272  tgqioo  21283  bndth  21436  htpyco2  21457  phtpyco2  21468  caubl  21724  caublcls  21725  bcthlem1  21741  bcthlem2  21742  bcthlem4  21744  bcthlem5  21745  ovolfioo  21857  ovolficc  21858  ovolficcss  21859  ovolfsval  21860  ovolctb  21879  ovoliunlem2  21892  ovolicc2lem1  21906  ovolicc2lem5  21910  ovolfs2  21958  ioorinv  21963  uniiccdif  21965  uniioovol  21966  uniiccvol  21967  uniioombllem2a  21969  uniioombllem2  21970  uniioombllem3a  21971  uniioombllem3  21972  uniioombllem4  21973  uniioombllem5  21974  uniioombllem6  21975  dyadovol  21980  dyadss  21981  dyaddisjlem  21982  dyadmaxlem  21984  dyadmbl  21987  opnmbllem  21988  itg1addlem4  22084  limccnp2  22274  dvbsss  22284  perfdvf  22285  dvdsmulf1o  23448  fsumdvdsmul  23449  fsumvma  23466  tglngne  23915  ltgseg  23960  tgelrnln  23988  edgov  24319  usgraexmplvtx  24380  usgraexmplcvtx  24383  usgraexmplcedg  24384  2wlkonot3v  24853  2spthonot3v  24854  isrgrac  24912  grposn  25195  rngosn  25384  imsdval  25570  ofresid  27460  ofoprabco  27483  xrofsup  27560  fvproj  27813  logb2aval  27987  elunirnmbfm  28202  sibfof  28260  oddpwdcv  28272  eulerpartlemgh  28295  cndprobval  28350  cvmlift2lem9  28734  cvmlift2lem10  28735  cvmlift2lem13  28738  cvmliftphtlem  28740  mclsrcl  28899  fvtransport  29658  fvray  29767  linedegen  29769  fvline  29770  opnmbllem0  30026  mblfinlem1  30027  mblfinlem2  30028  ftc1anc  30074  ftc2nc  30075  opropabco  30190  f1opr  30191  ismtyhmeolem  30276  heiborlem3  30285  heiborlem4  30286  heiborlem6  30288  heiborlem8  30290  fourierdlem42  31885  aovfundmoveq  32220  aovpcov0  32229  aovnuoveq  32230  aovvoveq  32231  aov0ov0  32232  aovovn0oveq  32233  aov0nbovbi  32234  aovov0bi  32235  uhgrasize  32347  usgrafisbaseALT  32394  usgrafisbaseALT2  32395  usgfis  32400  usgfisALT  32404  ovn0dmfun  32406  ovn0ssdmfun  32409  plusfreseq  32414  idfusubc0  32515  rhmsubclem2  32763  rhmsubcOLDlem2  32782  lmod1lem2  32959  lmod1lem3  32960  bj-finsumval0  34538
  Copyright terms: Public domain W3C validator