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

Definition df-ov 5781
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 9808). 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 5806 and ovprc2 5807. On the other hand, we often find uses for this definition when  F is a proper class, such as  +o in oav 6464.  F is normally equal to a class of nested ordered pairs of the form defined by df-oprab 5782. (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 5778 . 2  class  ( A F B )
51, 2cop 3603 . . 3  class  <. A ,  B >.
65, 3cfv 4659 . 2  class  ( F `
 <. A ,  B >. )
74, 6wceq 1619 1  wff  ( A F B )  =  ( F `  <. A ,  B >. )
Colors of variables: wff set class
This definition is referenced by:  oveq  5784  oveq1  5785  oveq2  5786  nfovd  5800  ovex  5803  ovssunirn  5804  ovprc  5805  fnotovb  5814  ffnov  5868  eqfnov  5870  fnov  5872  ovid  5884  ovidig  5885  ov  5887  ovigg  5888  ov6g  5905  ovg  5906  ovres  5907  fovrn  5910  fnrnov  5913  foov  5914  fnovrn  5915  funimassov  5917  ovelimab  5918  ovconst2  5919  oprssdm  5922  ndmovg  5923  elmpt2cl  5981  1st2val  6065  2nd2val  6066  ovmptss  6120  oprab2co  6124  curry1  6130  curry2  6133  algrflem  6144  ovtpos  6169  seqomlem1  6416  seqomlem4  6419  brwitnlem  6460  cantnfvalf  7320  fseqenlem1  7605  axdc4lem  8035  fpwwe  8222  canthwelem  8226  addpiord  8462  mulpiord  8463  addpqnq  8516  mulpqnq  8519  recmulnq  8542  dmrecnq  8546  cnref1o  10302  ixxssxr  10620  om2uzrdg  10971  uzrdgsuci  10975  swrd00  11402  cnrecnv  11601  sadcf  12592  smupf  12617  eucalgval  12700  eucalginv  12702  eucalglt  12703  eucalg  12705  vdwmc  12973  isstruct2  13105  isstruct  13106  prdsval  13303  prdsplusg  13306  prdsmulr  13307  prdsvsca  13308  prdshom  13314  imasaddvallem  13379  imasvscafn  13387  imasvscaval  13388  xpsff1o  13418  xpsaddlem  13425  xpsvsca  13429  xpsle  13431  comffval  13550  comfffval2  13552  comfeq  13557  isoval  13615  isssc  13645  isfuncd  13687  funcf2  13690  idfu2nd  13699  idfucl  13703  cofucl  13710  resfval2  13715  resf2nd  13717  funcres2b  13719  funcpropd  13722  homarcl  13808  homaval  13811  homarcl2  13815  arwhoma  13825  coapm  13851  catcco  13881  catcisolem  13886  xpcco  13905  xpcid  13911  xpcpropd  13930  evlfcllem  13943  evlfcl  13944  curf1cl  13950  curf2cl  13953  curfcl  13954  uncf1  13958  uncf2  13959  uncfcurf  13961  diag11  13965  diag12  13966  diag2  13967  curf2ndf  13969  hof2fval  13977  hofcl  13981  hofpropd  13989  yonedalem21  13995  yonedalem22  14000  yonedalem3b  14001  yonedalem3  14002  yonedainv  14003  yonffthlem  14004  plusffval  14327  gaid  14701  oppglsm  14901  efgmnvl  14971  efgval2  14981  vrgpinv  15026  frgpuptinv  15028  frgpuplem  15029  frgpup2  15033  frgpup3lem  15034  frgpnabllem1  15109  gsum2d  15171  gsum2d2lem  15172  gsumcom2  15174  eldprd  15187  dprd2dlem2  15223  dprd2dlem1  15224  dprd2da  15225  scaffval  15593  ipffval  16500  iccordt  16892  iscnp2  16917  ptbasfi  17224  txcnpi  17250  txdis1cn  17277  lmcn2  17291  xkococn  17302  cnmpt12f  17308  cnmpt21  17313  cnmpt2t  17315  cnmpt22  17316  cnmpt2k  17330  xkohmeo  17454  flfcnp2  17650  tmdcn2  17720  clssubg  17739  tgphaus  17747  divstgplem  17751  imasdsf1olem  17885  xpsdsval  17893  xmeterval  17926  comet  18007  txmetcnp  18041  nrmmetd  18045  nmfval  18059  isngp3  18068  ngpds  18073  tngnm  18115  qtopbaslem  18215  cnmetdval  18228  remetdval  18243  tgqioo  18254  bndth  18404  htpyco2  18425  phtpyco2  18436  caubl  18681  caublcls  18682  bcthlem1  18694  bcthlem2  18695  bcthlem4  18697  bcthlem5  18698  ovolfioo  18775  ovolficc  18776  ovolficcss  18777  ovolfsval  18778  ovolctb  18797  ovoliunlem2  18810  ovolicc2lem1  18824  ovolicc2lem5  18828  ovolfs2  18874  ioorinv  18879  uniiccdif  18881  uniioovol  18882  uniiccvol  18883  uniioombllem2a  18885  uniioombllem2  18886  uniioombllem3a  18887  uniioombllem3  18888  uniioombllem4  18889  uniioombllem5  18890  uniioombllem6  18891  dyadovol  18896  dyadss  18897  dyaddisjlem  18898  dyadmaxlem  18900  dyadmbl  18903  opnmbllem  18904  itg1addlem4  19002  limccnp2  19190  dvbsss  19200  perfdvf  19201  dvdsmulf1o  20382  fsumdvdsmul  20383  fsumvma  20400  grposn  20828  rngosn  21017  imsdval  21201  cvmlift2lem9  23200  cvmlift2lem10  23201  cvmlift2lem13  23204  cvmliftphtlem  23206  fvtransport  24016  fvray  24125  linedegen  24127  fvline  24128  oprssopvg  24386  fnovpop  24390  fnovrn2  24402  cbcpcp  24515  ltrcmp  24758  islimrs  24933  vecaddonto  25012  vecscmonto  25039  1ded  25091  1cat  25112  ishomb  25141  isfuna  25187  valtar  25236  cmpmor  25328  opropabco  25742  f1opr  25744  ismtyhmeolem  25881  heiborlem3  25890  heiborlem4  25891  heiborlem6  25893  heiborlem8  25895  mamudi  26814  mamudir  26815  mamuvs1  26816  mamuvs2  26817  matrcl  26819  logbval  27293
  Copyright terms: Public domain W3C validator