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

Definition df-ov 6308
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 10749). 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 6336 and ovprc2 6337. On the other hand, we often find uses for this definition when  F is a proper class, such as  +o in oav 7224.  F is normally equal to a class of nested ordered pairs of the form defined by df-oprab 6309. (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 6305 . 2  class  ( A F B )
51, 2cop 4004 . . 3  class  <. A ,  B >.
65, 3cfv 5601 . 2  class  ( F `
 <. A ,  B >. )
74, 6wceq 1437 1  wff  ( A F B )  =  ( F `  <. A ,  B >. )
Colors of variables: wff setvar class
This definition is referenced by:  oveq  6311  oveq1  6312  oveq2  6313  nfovd  6330  ovex  6333  ovssunirn  6334  ovprc  6335  csbov123  6339  csbov  6340  elovimad  6345  fnotovb  6346  ffnov  6414  eqfnov  6416  fnov  6418  ovid  6427  ovidig  6428  ov  6430  ovigg  6431  ov6g  6448  ovg  6449  ovres  6450  fovrn  6453  fnrnov  6456  foov  6457  fnovrn  6458  funimassov  6460  ovelimab  6461  ovima0  6462  ovconst2  6463  oprssdm  6464  nssdmovg  6465  ndmovg  6466  elmpt2cl  6525  1st2val  6833  2nd2val  6834  bropopvvv  6887  ovmptss  6888  oprab2co  6892  curry1  6899  curry2  6902  algrflem  6916  mpt2xeldm  6968  mpt2xopn0yelv  6970  mpt2xopxnop0  6972  ovtpos  6999  mpt2curryd  7027  seqomlem1  7178  seqomlem4  7181  brwitnlem  7220  cantnfvalf  8178  fseqenlem1  8462  axdc4lem  8892  fpwwe  9078  canthwelem  9082  addpiord  9316  mulpiord  9317  addpqnq  9370  mulpqnq  9373  recmulnq  9396  dmrecnq  9400  cnref1o  11304  ixxssxr  11654  om2uzrdg  12176  uzrdgsuci  12180  swrd00  12776  swrd0  12792  cnrecnv  13228  sadcf  14426  smupf  14451  eucalgval  14540  eucalginv  14542  eucalglt  14543  eucalg  14545  vdwmc  14927  isstruct2  15129  isstruct  15130  imasaddvallem  15434  imasvscafn  15442  imasvscaval  15443  xpsff1o  15473  xpsaddlem  15480  xpsvsca  15484  xpsle  15486  comffval  15603  comfffval2  15605  comfeq  15610  isoval  15669  brcic  15702  isssc  15724  isfuncd  15769  funcf2  15772  idfu2nd  15781  idfucl  15785  cofucl  15792  resfval2  15797  resf2nd  15799  funcres2b  15801  funcpropd  15804  homarcl  15922  homaval  15925  homarcl2  15929  arwhoma  15939  coapm  15965  catcco  15995  catcisolem  16000  xpcco  16067  xpcid  16073  xpcpropd  16092  evlfcllem  16105  evlfcl  16106  curf1cl  16112  curf2cl  16115  curfcl  16116  uncf1  16120  uncf2  16121  uncfcurf  16123  diag11  16127  diag12  16128  diag2  16129  curf2ndf  16131  hof2fval  16139  hofcl  16143  hofpropd  16151  yonedalem21  16157  yonedalem22  16162  yonedalem3b  16163  yonedalem3  16164  yonedainv  16165  yonffthlem  16166  joinval  16250  meetval  16264  plusffval  16492  mgm1  16499  sgrp1  16533  mnd1  16576  mnd1OLD  16577  mnd1id  16578  grp1  16757  gaid  16952  oppglsm  17293  efgmnvl  17363  efgval2  17373  vrgpinv  17418  frgpuptinv  17420  frgpuplem  17421  frgpup2  17425  frgpup3lem  17426  frgpnabllem1  17508  gsum2dlem1  17601  gsum2dlem2  17602  gsum2d  17603  gsum2d2lem  17604  gsumcom2  17606  eldprd  17635  dprd2dlem2  17672  dprd2dlem1  17673  dprd2da  17674  ring1  17829  scaffval  18108  ply1frcl  18906  ipffval  19213  mamudi  19426  mamudir  19427  mamuvs1  19428  mamuvs2  19429  matplusgcell  19456  matsubgcell  19457  matvscacell  19459  mat1dimmul  19499  mat1rhmelval  19503  mdetrlin  19625  mdetrsca  19626  pmatcoe1fsupp  19723  iccordt  20228  iscnp2  20253  ptbasfi  20594  txcnpi  20621  txdis1cn  20648  lmcn2  20662  xkococn  20673  cnmpt12f  20679  cnmpt21  20684  cnmpt2t  20686  cnmpt22  20687  cnmpt2k  20701  xkohmeo  20828  flfcnp2  21020  tmdcn2  21102  clssubg  21121  tgphaus  21129  qustgplem  21133  psmetxrge0  21327  imasdsf1olem  21386  xpsdsval  21394  xmeterval  21445  comet  21526  txmetcnp  21560  metustid  21567  metustsym  21568  metustexhalf  21569  blval2  21575  metuel2  21578  nrmmetd  21587  nmfval  21601  isngp3  21610  ngpds  21615  tngnm  21657  qtopbaslem  21777  cnmetdval  21789  remetdval  21805  tgqioo  21816  bndth  21984  htpyco2  22008  phtpyco2  22019  caubl  22275  caublcls  22276  bcthlem1  22290  bcthlem2  22291  bcthlem4  22293  bcthlem5  22294  ovolfioo  22418  ovolficc  22419  ovolficcss  22420  ovolfsval  22421  ovolctb  22441  ovoliunlem2  22454  ovolicc2lem1  22468  ovolicc2lem5  22473  ovolfs2  22521  ioorinv  22526  ioorinvOLD  22531  uniiccdif  22533  uniioovol  22534  uniiccvol  22535  uniioombllem2a  22537  uniioombllem2  22538  uniioombllem2OLD  22539  uniioombllem3a  22540  uniioombllem3  22541  uniioombllem4  22542  uniioombllem5  22543  uniioombllem6  22544  dyadovol  22549  dyadss  22550  dyaddisjlem  22551  dyadmaxlem  22553  dyadmbl  22556  opnmbllem  22557  itg1addlem4  22655  limccnp2  22845  dvbsss  22855  perfdvf  22856  dvdsmulf1o  24121  fsumdvdsmul  24122  fsumvma  24139  tglngne  24593  ltgseg  24639  tgelrnln  24673  edgov  25066  usgraexmplvtx  25128  usgraexmplcvtx  25131  usgraexmplcedg  25132  2wlkonot3v  25601  2spthonot3v  25602  isrgrac  25660  grposn  25941  rngosn  26130  imsdval  26316  ofresid  28245  ofoprabco  28269  xrofsup  28359  smatrcl  28630  smatlem  28631  fvproj  28667  elunirnmbfm  29083  sibfof  29181  oddpwdcv  29196  eulerpartlemgh  29219  cndprobval  29274  cvmlift2lem9  30042  cvmlift2lem10  30043  cvmlift2lem13  30046  cvmliftphtlem  30048  mclsrcl  30207  fvtransport  30804  fvray  30913  linedegen  30915  fvline  30916  bj-finsumval0  31666  icoreunrn  31726  relowlpssretop  31731  finxpreclem1  31745  finxpreclem2  31746  finxpreclem3  31749  finxpreclem5  31751  opnmbllem0  31940  mblfinlem1  31941  mblfinlem2  31942  ftc1anc  31989  ftc2nc  31990  opropabco  32014  f1opr  32015  ismtyhmeolem  32100  heiborlem3  32109  heiborlem4  32110  heiborlem6  32112  heiborlem8  32114  fvovco  37430  fourierdlem42  37952  fourierdlem42OLD  37953  aovfundmoveq  38553  aovpcov0  38562  aovnuoveq  38563  aovvoveq  38564  aov0ov0  38565  aovovn0oveq  38566  aov0nbovbi  38567  aovov0bi  38568  pfx00  38795  pfx0  38796  opvtxov  38939  opiedgov  38942  edgaov  39031  uhgrasize  39325  usgrafisbaseALT  39372  usgrafisbaseALT2  39373  usgfis  39378  usgfisALT  39382  ovn0dmfun  39384  ovn0ssdmfun  39387  plusfreseq  39392  idfusubc0  39485  rhmsubclem2  39709  rhmsubcALTVlem2  39728  lmod1lem2  39903  lmod1lem3  39904  logb2aval  40115
  Copyright terms: Public domain W3C validator