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

Definition df-ov 6043
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 10067). 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 6068 and ovprc2 6069. On the other hand, we often find uses for this definition when  F is a proper class, such as  +o in oav 6714.  F is normally equal to a class of nested ordered pairs of the form defined by df-oprab 6044. (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 6040 . 2  class  ( A F B )
51, 2cop 3777 . . 3  class  <. A ,  B >.
65, 3cfv 5413 . 2  class  ( F `
 <. A ,  B >. )
74, 6wceq 1649 1  wff  ( A F B )  =  ( F `  <. A ,  B >. )
Colors of variables: wff set class
This definition is referenced by:  oveq  6046  oveq1  6047  oveq2  6048  nfovd  6062  ovex  6065  ovssunirn  6066  ovprc  6067  fnotovb  6076  ffnov  6133  eqfnov  6135  fnov  6137  ovid  6149  ovidig  6150  ov  6152  ovigg  6153  ov6g  6170  ovg  6171  ovres  6172  fovrn  6175  fnrnov  6178  foov  6179  fnovrn  6180  funimassov  6182  ovelimab  6183  ovconst2  6184  oprssdm  6187  nssdmovg  6188  ndmovg  6189  elmpt2cl  6247  1st2val  6331  2nd2val  6332  bropopvvv  6385  ovmptss  6387  oprab2co  6391  curry1  6397  curry2  6400  algrflem  6414  mpt2xopn0yelv  6423  mpt2xopxnop0  6425  ovtpos  6453  seqomlem1  6666  seqomlem4  6669  brwitnlem  6710  cantnfvalf  7576  fseqenlem1  7861  axdc4lem  8291  fpwwe  8477  canthwelem  8481  addpiord  8717  mulpiord  8718  addpqnq  8771  mulpqnq  8774  recmulnq  8797  dmrecnq  8801  cnref1o  10563  ixxssxr  10884  om2uzrdg  11251  uzrdgsuci  11255  swrd00  11720  cnrecnv  11925  sadcf  12920  smupf  12945  eucalgval  13028  eucalginv  13030  eucalglt  13031  eucalg  13033  vdwmc  13301  isstruct2  13433  isstruct  13434  imasaddvallem  13709  imasvscafn  13717  imasvscaval  13718  xpsff1o  13748  xpsaddlem  13755  xpsvsca  13759  xpsle  13761  comffval  13880  comfffval2  13882  comfeq  13887  isoval  13945  isssc  13975  isfuncd  14017  funcf2  14020  idfu2nd  14029  idfucl  14033  cofucl  14040  resfval2  14045  resf2nd  14047  funcres2b  14049  funcpropd  14052  homarcl  14138  homaval  14141  homarcl2  14145  arwhoma  14155  coapm  14181  catcco  14211  catcisolem  14216  xpcco  14235  xpcid  14241  xpcpropd  14260  evlfcllem  14273  evlfcl  14274  curf1cl  14280  curf2cl  14283  curfcl  14284  uncf1  14288  uncf2  14289  uncfcurf  14291  diag11  14295  diag12  14296  diag2  14297  curf2ndf  14299  hof2fval  14307  hofcl  14311  hofpropd  14319  yonedalem21  14325  yonedalem22  14330  yonedalem3b  14331  yonedalem3  14332  yonedainv  14333  yonffthlem  14334  plusffval  14657  gaid  15031  oppglsm  15231  efgmnvl  15301  efgval2  15311  vrgpinv  15356  frgpuptinv  15358  frgpuplem  15359  frgpup2  15363  frgpup3lem  15364  frgpnabllem1  15439  gsum2d  15501  gsum2d2lem  15502  gsumcom2  15504  eldprd  15517  dprd2dlem2  15553  dprd2dlem1  15554  dprd2da  15555  scaffval  15923  ipffval  16834  iccordt  17232  iscnp2  17257  ptbasfi  17566  txcnpi  17593  txdis1cn  17620  lmcn2  17634  xkococn  17645  cnmpt12f  17651  cnmpt21  17656  cnmpt2t  17658  cnmpt22  17659  cnmpt2k  17673  xkohmeo  17800  flfcnp2  17992  tmdcn2  18072  clssubg  18091  tgphaus  18099  divstgplem  18103  psmetxrge0  18297  imasdsf1olem  18356  xpsdsval  18364  xmeterval  18415  comet  18496  txmetcnp  18530  metustidOLD  18542  metustid  18543  metustsymOLD  18544  metustsym  18545  metustexhalfOLD  18546  metustexhalf  18547  blval2  18558  metuel2  18562  nrmmetd  18575  nmfval  18589  isngp3  18598  ngpds  18603  tngnm  18645  qtopbaslem  18745  cnmetdval  18758  remetdval  18773  tgqioo  18784  bndth  18936  htpyco2  18957  phtpyco2  18968  caubl  19213  caublcls  19214  bcthlem1  19230  bcthlem2  19231  bcthlem4  19233  bcthlem5  19234  ovolfioo  19317  ovolficc  19318  ovolficcss  19319  ovolfsval  19320  ovolctb  19339  ovoliunlem2  19352  ovolicc2lem1  19366  ovolicc2lem5  19370  ovolfs2  19416  ioorinv  19421  uniiccdif  19423  uniioovol  19424  uniiccvol  19425  uniioombllem2a  19427  uniioombllem2  19428  uniioombllem3a  19429  uniioombllem3  19430  uniioombllem4  19431  uniioombllem5  19432  uniioombllem6  19433  dyadovol  19438  dyadss  19439  dyaddisjlem  19440  dyadmaxlem  19442  dyadmbl  19445  opnmbllem  19446  itg1addlem4  19544  limccnp2  19732  dvbsss  19742  perfdvf  19743  dvdsmulf1o  20932  fsumdvdsmul  20933  fsumvma  20950  grposn  21756  rngosn  21945  imsdval  22131  elovimad  24004  ofresid  24008  ofoprabco  24032  xrofsup  24079  logb2aval  24344  elunirnmbfm  24556  sibfof  24607  cndprobval  24644  cvmlift2lem9  24951  cvmlift2lem10  24952  cvmlift2lem13  24955  cvmliftphtlem  24957  fvtransport  25870  fvray  25979  linedegen  25981  fvline  25982  mblfinlem  26143  opropabco  26315  f1opr  26316  ismtyhmeolem  26403  heiborlem3  26412  heiborlem4  26413  heiborlem6  26415  heiborlem8  26417  mamudi  27329  mamudir  27330  mamuvs1  27331  mamuvs2  27332  aovfundmoveq  27912  aovpcov0  27921  aovnuoveq  27922  aovvoveq  27923  aov0ov0  27924  aovovn0oveq  27925  aov0nbovbi  27926  aovov0bi  27927  2wlkonot3v  28072  2spthonot3v  28073
  Copyright terms: Public domain W3C validator