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

Definition df-ov 6084
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 10111). 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 6109 and ovprc2 6110. On the other hand, we often find uses for this definition when  F is a proper class, such as  +o in oav 6755.  F is normally equal to a class of nested ordered pairs of the form defined by df-oprab 6085. (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 6081 . 2  class  ( A F B )
51, 2cop 3817 . . 3  class  <. A ,  B >.
65, 3cfv 5454 . 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  6087  oveq1  6088  oveq2  6089  nfovd  6103  ovex  6106  ovssunirn  6107  ovprc  6108  fnotovb  6117  ffnov  6174  eqfnov  6176  fnov  6178  ovid  6190  ovidig  6191  ov  6193  ovigg  6194  ov6g  6211  ovg  6212  ovres  6213  fovrn  6216  fnrnov  6219  foov  6220  fnovrn  6221  funimassov  6223  ovelimab  6224  ovconst2  6225  oprssdm  6228  nssdmovg  6229  ndmovg  6230  elmpt2cl  6288  1st2val  6372  2nd2val  6373  bropopvvv  6426  ovmptss  6428  oprab2co  6432  curry1  6438  curry2  6441  algrflem  6455  mpt2xopn0yelv  6464  mpt2xopxnop0  6466  ovtpos  6494  seqomlem1  6707  seqomlem4  6710  brwitnlem  6751  cantnfvalf  7620  fseqenlem1  7905  axdc4lem  8335  fpwwe  8521  canthwelem  8525  addpiord  8761  mulpiord  8762  addpqnq  8815  mulpqnq  8818  recmulnq  8841  dmrecnq  8845  cnref1o  10607  ixxssxr  10928  om2uzrdg  11296  uzrdgsuci  11300  swrd00  11765  cnrecnv  11970  sadcf  12965  smupf  12990  eucalgval  13073  eucalginv  13075  eucalglt  13076  eucalg  13078  vdwmc  13346  isstruct2  13478  isstruct  13479  imasaddvallem  13754  imasvscafn  13762  imasvscaval  13763  xpsff1o  13793  xpsaddlem  13800  xpsvsca  13804  xpsle  13806  comffval  13925  comfffval2  13927  comfeq  13932  isoval  13990  isssc  14020  isfuncd  14062  funcf2  14065  idfu2nd  14074  idfucl  14078  cofucl  14085  resfval2  14090  resf2nd  14092  funcres2b  14094  funcpropd  14097  homarcl  14183  homaval  14186  homarcl2  14190  arwhoma  14200  coapm  14226  catcco  14256  catcisolem  14261  xpcco  14280  xpcid  14286  xpcpropd  14305  evlfcllem  14318  evlfcl  14319  curf1cl  14325  curf2cl  14328  curfcl  14329  uncf1  14333  uncf2  14334  uncfcurf  14336  diag11  14340  diag12  14341  diag2  14342  curf2ndf  14344  hof2fval  14352  hofcl  14356  hofpropd  14364  yonedalem21  14370  yonedalem22  14375  yonedalem3b  14376  yonedalem3  14377  yonedainv  14378  yonffthlem  14379  plusffval  14702  gaid  15076  oppglsm  15276  efgmnvl  15346  efgval2  15356  vrgpinv  15401  frgpuptinv  15403  frgpuplem  15404  frgpup2  15408  frgpup3lem  15409  frgpnabllem1  15484  gsum2d  15546  gsum2d2lem  15547  gsumcom2  15549  eldprd  15562  dprd2dlem2  15598  dprd2dlem1  15599  dprd2da  15600  scaffval  15968  ipffval  16879  iccordt  17278  iscnp2  17303  ptbasfi  17613  txcnpi  17640  txdis1cn  17667  lmcn2  17681  xkococn  17692  cnmpt12f  17698  cnmpt21  17703  cnmpt2t  17705  cnmpt22  17706  cnmpt2k  17720  xkohmeo  17847  flfcnp2  18039  tmdcn2  18119  clssubg  18138  tgphaus  18146  divstgplem  18150  psmetxrge0  18344  imasdsf1olem  18403  xpsdsval  18411  xmeterval  18462  comet  18543  txmetcnp  18577  metustidOLD  18589  metustid  18590  metustsymOLD  18591  metustsym  18592  metustexhalfOLD  18593  metustexhalf  18594  blval2  18605  metuel2  18609  nrmmetd  18622  nmfval  18636  isngp3  18645  ngpds  18650  tngnm  18692  qtopbaslem  18792  cnmetdval  18805  remetdval  18820  tgqioo  18831  bndth  18983  htpyco2  19004  phtpyco2  19015  caubl  19260  caublcls  19261  bcthlem1  19277  bcthlem2  19278  bcthlem4  19280  bcthlem5  19281  ovolfioo  19364  ovolficc  19365  ovolficcss  19366  ovolfsval  19367  ovolctb  19386  ovoliunlem2  19399  ovolicc2lem1  19413  ovolicc2lem5  19417  ovolfs2  19463  ioorinv  19468  uniiccdif  19470  uniioovol  19471  uniiccvol  19472  uniioombllem2a  19474  uniioombllem2  19475  uniioombllem3a  19476  uniioombllem3  19477  uniioombllem4  19478  uniioombllem5  19479  uniioombllem6  19480  dyadovol  19485  dyadss  19486  dyaddisjlem  19487  dyadmaxlem  19489  dyadmbl  19492  opnmbllem  19493  itg1addlem4  19591  limccnp2  19779  dvbsss  19789  perfdvf  19790  dvdsmulf1o  20979  fsumdvdsmul  20980  fsumvma  20997  grposn  21803  rngosn  21992  imsdval  22178  elovimad  24051  ofresid  24055  ofoprabco  24079  xrofsup  24126  logb2aval  24391  elunirnmbfm  24603  sibfof  24654  cndprobval  24691  cvmlift2lem9  24998  cvmlift2lem10  24999  cvmlift2lem13  25002  cvmliftphtlem  25004  fvtransport  25966  fvray  26075  linedegen  26077  fvline  26078  opnmbllem0  26242  mblfinlem1  26243  mblfinlem2  26244  ftc1anc  26288  ftc2nc  26289  opropabco  26425  f1opr  26426  ismtyhmeolem  26513  heiborlem3  26522  heiborlem4  26523  heiborlem6  26525  heiborlem8  26527  mamudi  27438  mamudir  27439  mamuvs1  27440  mamuvs2  27441  aovfundmoveq  28021  aovpcov0  28030  aovnuoveq  28031  aovvoveq  28032  aov0ov0  28033  aovovn0oveq  28034  aov0nbovbi  28035  aovov0bi  28036  2wlkonot3v  28342  2spthonot3v  28343
  Copyright terms: Public domain W3C validator