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

Definition df-ov 6076
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 10103). 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 6101 and ovprc2 6102. On the other hand, we often find uses for this definition when  F is a proper class, such as  +o in oav 6747.  F is normally equal to a class of nested ordered pairs of the form defined by df-oprab 6077. (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 6073 . 2  class  ( A F B )
51, 2cop 3809 . . 3  class  <. A ,  B >.
65, 3cfv 5446 . 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  6079  oveq1  6080  oveq2  6081  nfovd  6095  ovex  6098  ovssunirn  6099  ovprc  6100  fnotovb  6109  ffnov  6166  eqfnov  6168  fnov  6170  ovid  6182  ovidig  6183  ov  6185  ovigg  6186  ov6g  6203  ovg  6204  ovres  6205  fovrn  6208  fnrnov  6211  foov  6212  fnovrn  6213  funimassov  6215  ovelimab  6216  ovconst2  6217  oprssdm  6220  nssdmovg  6221  ndmovg  6222  elmpt2cl  6280  1st2val  6364  2nd2val  6365  bropopvvv  6418  ovmptss  6420  oprab2co  6424  curry1  6430  curry2  6433  algrflem  6447  mpt2xopn0yelv  6456  mpt2xopxnop0  6458  ovtpos  6486  seqomlem1  6699  seqomlem4  6702  brwitnlem  6743  cantnfvalf  7612  fseqenlem1  7897  axdc4lem  8327  fpwwe  8513  canthwelem  8517  addpiord  8753  mulpiord  8754  addpqnq  8807  mulpqnq  8810  recmulnq  8833  dmrecnq  8837  cnref1o  10599  ixxssxr  10920  om2uzrdg  11288  uzrdgsuci  11292  swrd00  11757  cnrecnv  11962  sadcf  12957  smupf  12982  eucalgval  13065  eucalginv  13067  eucalglt  13068  eucalg  13070  vdwmc  13338  isstruct2  13470  isstruct  13471  imasaddvallem  13746  imasvscafn  13754  imasvscaval  13755  xpsff1o  13785  xpsaddlem  13792  xpsvsca  13796  xpsle  13798  comffval  13917  comfffval2  13919  comfeq  13924  isoval  13982  isssc  14012  isfuncd  14054  funcf2  14057  idfu2nd  14066  idfucl  14070  cofucl  14077  resfval2  14082  resf2nd  14084  funcres2b  14086  funcpropd  14089  homarcl  14175  homaval  14178  homarcl2  14182  arwhoma  14192  coapm  14218  catcco  14248  catcisolem  14253  xpcco  14272  xpcid  14278  xpcpropd  14297  evlfcllem  14310  evlfcl  14311  curf1cl  14317  curf2cl  14320  curfcl  14321  uncf1  14325  uncf2  14326  uncfcurf  14328  diag11  14332  diag12  14333  diag2  14334  curf2ndf  14336  hof2fval  14344  hofcl  14348  hofpropd  14356  yonedalem21  14362  yonedalem22  14367  yonedalem3b  14368  yonedalem3  14369  yonedainv  14370  yonffthlem  14371  plusffval  14694  gaid  15068  oppglsm  15268  efgmnvl  15338  efgval2  15348  vrgpinv  15393  frgpuptinv  15395  frgpuplem  15396  frgpup2  15400  frgpup3lem  15401  frgpnabllem1  15476  gsum2d  15538  gsum2d2lem  15539  gsumcom2  15541  eldprd  15554  dprd2dlem2  15590  dprd2dlem1  15591  dprd2da  15592  scaffval  15960  ipffval  16871  iccordt  17270  iscnp2  17295  ptbasfi  17605  txcnpi  17632  txdis1cn  17659  lmcn2  17673  xkococn  17684  cnmpt12f  17690  cnmpt21  17695  cnmpt2t  17697  cnmpt22  17698  cnmpt2k  17712  xkohmeo  17839  flfcnp2  18031  tmdcn2  18111  clssubg  18130  tgphaus  18138  divstgplem  18142  psmetxrge0  18336  imasdsf1olem  18395  xpsdsval  18403  xmeterval  18454  comet  18535  txmetcnp  18569  metustidOLD  18581  metustid  18582  metustsymOLD  18583  metustsym  18584  metustexhalfOLD  18585  metustexhalf  18586  blval2  18597  metuel2  18601  nrmmetd  18614  nmfval  18628  isngp3  18637  ngpds  18642  tngnm  18684  qtopbaslem  18784  cnmetdval  18797  remetdval  18812  tgqioo  18823  bndth  18975  htpyco2  18996  phtpyco2  19007  caubl  19252  caublcls  19253  bcthlem1  19269  bcthlem2  19270  bcthlem4  19272  bcthlem5  19273  ovolfioo  19356  ovolficc  19357  ovolficcss  19358  ovolfsval  19359  ovolctb  19378  ovoliunlem2  19391  ovolicc2lem1  19405  ovolicc2lem5  19409  ovolfs2  19455  ioorinv  19460  uniiccdif  19462  uniioovol  19463  uniiccvol  19464  uniioombllem2a  19466  uniioombllem2  19467  uniioombllem3a  19468  uniioombllem3  19469  uniioombllem4  19470  uniioombllem5  19471  uniioombllem6  19472  dyadovol  19477  dyadss  19478  dyaddisjlem  19479  dyadmaxlem  19481  dyadmbl  19484  opnmbllem  19485  itg1addlem4  19583  limccnp2  19771  dvbsss  19781  perfdvf  19782  dvdsmulf1o  20971  fsumdvdsmul  20972  fsumvma  20989  grposn  21795  rngosn  21984  imsdval  22170  elovimad  24043  ofresid  24047  ofoprabco  24071  xrofsup  24118  logb2aval  24383  elunirnmbfm  24595  sibfof  24646  cndprobval  24683  cvmlift2lem9  24990  cvmlift2lem10  24991  cvmlift2lem13  24994  cvmliftphtlem  24996  fvtransport  25958  fvray  26067  linedegen  26069  fvline  26070  mblfinlem  26234  ftc1anc  26278  ftc2nc  26279  opropabco  26416  f1opr  26417  ismtyhmeolem  26504  heiborlem3  26513  heiborlem4  26514  heiborlem6  26516  heiborlem8  26518  mamudi  27429  mamudir  27430  mamuvs1  27431  mamuvs2  27432  aovfundmoveq  28012  aovpcov0  28021  aovnuoveq  28022  aovvoveq  28023  aov0ov0  28024  aovovn0oveq  28025  aov0nbovbi  28026  aovov0bi  28027  2wlkonot3v  28295  2spthonot3v  28296
  Copyright terms: Public domain W3C validator