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

Definition df-ov 6070
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 10095). 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 6095 and ovprc2 6096. On the other hand, we often find uses for this definition when  F is a proper class, such as  +o in oav 6741.  F is normally equal to a class of nested ordered pairs of the form defined by df-oprab 6071. (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 6067 . 2  class  ( A F B )
51, 2cop 3804 . . 3  class  <. A ,  B >.
65, 3cfv 5440 . 2  class  ( F `
 <. A ,  B >. )
74, 6wceq 1652 1  wff  ( A F B )  =  ( F `  <. A ,  B >. )
Colors of variables: wff set class
This definition is referenced by:  oveq  6073  oveq1  6074  oveq2  6075  nfovd  6089  ovex  6092  ovssunirn  6093  ovprc  6094  fnotovb  6103  ffnov  6160  eqfnov  6162  fnov  6164  ovid  6176  ovidig  6177  ov  6179  ovigg  6180  ov6g  6197  ovg  6198  ovres  6199  fovrn  6202  fnrnov  6205  foov  6206  fnovrn  6207  funimassov  6209  ovelimab  6210  ovconst2  6211  oprssdm  6214  nssdmovg  6215  ndmovg  6216  elmpt2cl  6274  1st2val  6358  2nd2val  6359  bropopvvv  6412  ovmptss  6414  oprab2co  6418  curry1  6424  curry2  6427  algrflem  6441  mpt2xopn0yelv  6450  mpt2xopxnop0  6452  ovtpos  6480  seqomlem1  6693  seqomlem4  6696  brwitnlem  6737  cantnfvalf  7604  fseqenlem1  7889  axdc4lem  8319  fpwwe  8505  canthwelem  8509  addpiord  8745  mulpiord  8746  addpqnq  8799  mulpqnq  8802  recmulnq  8825  dmrecnq  8829  cnref1o  10591  ixxssxr  10912  om2uzrdg  11279  uzrdgsuci  11283  swrd00  11748  cnrecnv  11953  sadcf  12948  smupf  12973  eucalgval  13056  eucalginv  13058  eucalglt  13059  eucalg  13061  vdwmc  13329  isstruct2  13461  isstruct  13462  imasaddvallem  13737  imasvscafn  13745  imasvscaval  13746  xpsff1o  13776  xpsaddlem  13783  xpsvsca  13787  xpsle  13789  comffval  13908  comfffval2  13910  comfeq  13915  isoval  13973  isssc  14003  isfuncd  14045  funcf2  14048  idfu2nd  14057  idfucl  14061  cofucl  14068  resfval2  14073  resf2nd  14075  funcres2b  14077  funcpropd  14080  homarcl  14166  homaval  14169  homarcl2  14173  arwhoma  14183  coapm  14209  catcco  14239  catcisolem  14244  xpcco  14263  xpcid  14269  xpcpropd  14288  evlfcllem  14301  evlfcl  14302  curf1cl  14308  curf2cl  14311  curfcl  14312  uncf1  14316  uncf2  14317  uncfcurf  14319  diag11  14323  diag12  14324  diag2  14325  curf2ndf  14327  hof2fval  14335  hofcl  14339  hofpropd  14347  yonedalem21  14353  yonedalem22  14358  yonedalem3b  14359  yonedalem3  14360  yonedainv  14361  yonffthlem  14362  plusffval  14685  gaid  15059  oppglsm  15259  efgmnvl  15329  efgval2  15339  vrgpinv  15384  frgpuptinv  15386  frgpuplem  15387  frgpup2  15391  frgpup3lem  15392  frgpnabllem1  15467  gsum2d  15529  gsum2d2lem  15530  gsumcom2  15532  eldprd  15545  dprd2dlem2  15581  dprd2dlem1  15582  dprd2da  15583  scaffval  15951  ipffval  16862  iccordt  17261  iscnp2  17286  ptbasfi  17596  txcnpi  17623  txdis1cn  17650  lmcn2  17664  xkococn  17675  cnmpt12f  17681  cnmpt21  17686  cnmpt2t  17688  cnmpt22  17689  cnmpt2k  17703  xkohmeo  17830  flfcnp2  18022  tmdcn2  18102  clssubg  18121  tgphaus  18129  divstgplem  18133  psmetxrge0  18327  imasdsf1olem  18386  xpsdsval  18394  xmeterval  18445  comet  18526  txmetcnp  18560  metustidOLD  18572  metustid  18573  metustsymOLD  18574  metustsym  18575  metustexhalfOLD  18576  metustexhalf  18577  blval2  18588  metuel2  18592  nrmmetd  18605  nmfval  18619  isngp3  18628  ngpds  18633  tngnm  18675  qtopbaslem  18775  cnmetdval  18788  remetdval  18803  tgqioo  18814  bndth  18966  htpyco2  18987  phtpyco2  18998  caubl  19243  caublcls  19244  bcthlem1  19260  bcthlem2  19261  bcthlem4  19263  bcthlem5  19264  ovolfioo  19347  ovolficc  19348  ovolficcss  19349  ovolfsval  19350  ovolctb  19369  ovoliunlem2  19382  ovolicc2lem1  19396  ovolicc2lem5  19400  ovolfs2  19446  ioorinv  19451  uniiccdif  19453  uniioovol  19454  uniiccvol  19455  uniioombllem2a  19457  uniioombllem2  19458  uniioombllem3a  19459  uniioombllem3  19460  uniioombllem4  19461  uniioombllem5  19462  uniioombllem6  19463  dyadovol  19468  dyadss  19469  dyaddisjlem  19470  dyadmaxlem  19472  dyadmbl  19475  opnmbllem  19476  itg1addlem4  19574  limccnp2  19762  dvbsss  19772  perfdvf  19773  dvdsmulf1o  20962  fsumdvdsmul  20963  fsumvma  20980  grposn  21786  rngosn  21975  imsdval  22161  elovimad  24034  ofresid  24038  ofoprabco  24062  xrofsup  24109  logb2aval  24374  elunirnmbfm  24586  sibfof  24637  cndprobval  24674  cvmlift2lem9  24981  cvmlift2lem10  24982  cvmlift2lem13  24985  cvmliftphtlem  24987  fvtransport  25909  fvray  26018  linedegen  26020  fvline  26021  mblfinlem  26185  opropabco  26357  f1opr  26358  ismtyhmeolem  26445  heiborlem3  26454  heiborlem4  26455  heiborlem6  26457  heiborlem8  26459  mamudi  27371  mamudir  27372  mamuvs1  27373  mamuvs2  27374  aovfundmoveq  27954  aovpcov0  27963  aovnuoveq  27964  aovvoveq  27965  aov0ov0  27966  aovovn0oveq  27967  aov0nbovbi  27968  aovov0bi  27969  2wlkonot3v  28114  2spthonot3v  28115
  Copyright terms: Public domain W3C validator