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

Definition df-ov 5877
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 9871). 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 5902 and ovprc2 5903. On the other hand, we often find uses for this definition when  F is a proper class, such as  +o in oav 6526.  F is normally equal to a class of nested ordered pairs of the form defined by df-oprab 5878. (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 5874 . 2  class  ( A F B )
51, 2cop 3656 . . 3  class  <. A ,  B >.
65, 3cfv 5271 . 2  class  ( F `
 <. A ,  B >. )
74, 6wceq 1632 1  wff  ( A F B )  =  ( F `  <. A ,  B >. )
Colors of variables: wff set class
This definition is referenced by:  oveq  5880  oveq1  5881  oveq2  5882  nfovd  5896  ovex  5899  ovssunirn  5900  ovprc  5901  fnotovb  5910  ffnov  5964  eqfnov  5966  fnov  5968  ovid  5980  ovidig  5981  ov  5983  ovigg  5984  ov6g  6001  ovg  6002  ovres  6003  fovrn  6006  fnrnov  6009  foov  6010  fnovrn  6011  funimassov  6013  ovelimab  6014  ovconst2  6015  oprssdm  6018  ndmovg  6019  elmpt2cl  6077  1st2val  6161  2nd2val  6162  ovmptss  6216  oprab2co  6220  curry1  6226  curry2  6229  algrflem  6240  ovtpos  6265  seqomlem1  6478  seqomlem4  6481  brwitnlem  6522  cantnfvalf  7382  fseqenlem1  7667  axdc4lem  8097  fpwwe  8284  canthwelem  8288  addpiord  8524  mulpiord  8525  addpqnq  8578  mulpqnq  8581  recmulnq  8604  dmrecnq  8608  cnref1o  10365  ixxssxr  10684  om2uzrdg  11035  uzrdgsuci  11039  swrd00  11467  cnrecnv  11666  sadcf  12660  smupf  12685  eucalgval  12768  eucalginv  12770  eucalglt  12771  eucalg  12773  vdwmc  13041  isstruct2  13173  isstruct  13174  prdsval  13371  prdsplusg  13374  prdsmulr  13375  prdsvsca  13376  prdshom  13382  imasaddvallem  13447  imasvscafn  13455  imasvscaval  13456  xpsff1o  13486  xpsaddlem  13493  xpsvsca  13497  xpsle  13499  comffval  13618  comfffval2  13620  comfeq  13625  isoval  13683  isssc  13713  isfuncd  13755  funcf2  13758  idfu2nd  13767  idfucl  13771  cofucl  13778  resfval2  13783  resf2nd  13785  funcres2b  13787  funcpropd  13790  homarcl  13876  homaval  13879  homarcl2  13883  arwhoma  13893  coapm  13919  catcco  13949  catcisolem  13954  xpcco  13973  xpcid  13979  xpcpropd  13998  evlfcllem  14011  evlfcl  14012  curf1cl  14018  curf2cl  14021  curfcl  14022  uncf1  14026  uncf2  14027  uncfcurf  14029  diag11  14033  diag12  14034  diag2  14035  curf2ndf  14037  hof2fval  14045  hofcl  14049  hofpropd  14057  yonedalem21  14063  yonedalem22  14068  yonedalem3b  14069  yonedalem3  14070  yonedainv  14071  yonffthlem  14072  plusffval  14395  gaid  14769  oppglsm  14969  efgmnvl  15039  efgval2  15049  vrgpinv  15094  frgpuptinv  15096  frgpuplem  15097  frgpup2  15101  frgpup3lem  15102  frgpnabllem1  15177  gsum2d  15239  gsum2d2lem  15240  gsumcom2  15242  eldprd  15255  dprd2dlem2  15291  dprd2dlem1  15292  dprd2da  15293  scaffval  15661  ipffval  16568  iccordt  16960  iscnp2  16985  ptbasfi  17292  txcnpi  17318  txdis1cn  17345  lmcn2  17359  xkococn  17370  cnmpt12f  17376  cnmpt21  17381  cnmpt2t  17383  cnmpt22  17384  cnmpt2k  17398  xkohmeo  17522  flfcnp2  17718  tmdcn2  17788  clssubg  17807  tgphaus  17815  divstgplem  17819  imasdsf1olem  17953  xpsdsval  17961  xmeterval  17994  comet  18075  txmetcnp  18109  nrmmetd  18113  nmfval  18127  isngp3  18136  ngpds  18141  tngnm  18183  qtopbaslem  18283  cnmetdval  18296  remetdval  18311  tgqioo  18322  bndth  18472  htpyco2  18493  phtpyco2  18504  caubl  18749  caublcls  18750  bcthlem1  18762  bcthlem2  18763  bcthlem4  18765  bcthlem5  18766  ovolfioo  18843  ovolficc  18844  ovolficcss  18845  ovolfsval  18846  ovolctb  18865  ovoliunlem2  18878  ovolicc2lem1  18892  ovolicc2lem5  18896  ovolfs2  18942  ioorinv  18947  uniiccdif  18949  uniioovol  18950  uniiccvol  18951  uniioombllem2a  18953  uniioombllem2  18954  uniioombllem3a  18955  uniioombllem3  18956  uniioombllem4  18957  uniioombllem5  18958  uniioombllem6  18959  dyadovol  18964  dyadss  18965  dyaddisjlem  18966  dyadmaxlem  18968  dyadmbl  18971  opnmbllem  18972  itg1addlem4  19070  limccnp2  19258  dvbsss  19268  perfdvf  19269  dvdsmulf1o  20450  fsumdvdsmul  20451  fsumvma  20468  grposn  20898  rngosn  21087  imsdval  21271  elovimad  23220  ofoprabco  23247  xrofsup  23270  logb2aval  23408  ismbfm  23572  cndprobval  23651  cvmlift2lem9  23857  cvmlift2lem10  23858  cvmlift2lem13  23861  cvmliftphtlem  23863  fvtransport  24727  fvray  24836  linedegen  24838  fvline  24839  oprssopvg  25137  fnovpop  25141  fnovrn2  25153  cbcpcp  25265  ltrcmp  25508  islimrs  25683  vecaddonto  25762  vecscmonto  25789  1ded  25841  1cat  25862  ishomb  25891  isfuna  25937  valtar  25986  cmpmor  26078  opropabco  26492  f1opr  26494  ismtyhmeolem  26631  heiborlem3  26640  heiborlem4  26641  heiborlem6  26643  heiborlem8  26645  mamudi  27564  mamudir  27565  mamuvs1  27566  mamuvs2  27567  matrcl  27569  aovfundmoveq  28149  aovpcov0  28158  aovnuoveq  28159  aovvoveq  28160  aov0ov0  28161  aovovn0oveq  28162  aov0nbovbi  28163  aovov0bi  28164  nssdmovg  28194  mpt2xopn0yelv  28195  mpt2xopxnop0  28197  nbgrael  28275  trlonprop  28341
  Copyright terms: Public domain W3C validator