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

Definition df-ov 6087
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 10116). 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 6112 and ovprc2 6113. On the other hand, we often find uses for this definition when  F is a proper class, such as  +o in oav 6758.  F is normally equal to a class of nested ordered pairs of the form defined by df-oprab 6088. (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 6084 . 2  class  ( A F B )
51, 2cop 3819 . . 3  class  <. A ,  B >.
65, 3cfv 5457 . 2  class  ( F `
 <. A ,  B >. )
74, 6wceq 1653 1  wff  ( A F B )  =  ( F `  <. A ,  B >. )
Colors of variables: wff set class
This definition is referenced by:  oveq  6090  oveq1  6091  oveq2  6092  nfovd  6106  ovex  6109  ovssunirn  6110  ovprc  6111  fnotovb  6120  ffnov  6177  eqfnov  6179  fnov  6181  ovid  6193  ovidig  6194  ov  6196  ovigg  6197  ov6g  6214  ovg  6215  ovres  6216  fovrn  6219  fnrnov  6222  foov  6223  fnovrn  6224  funimassov  6226  ovelimab  6227  ovconst2  6228  oprssdm  6231  nssdmovg  6232  ndmovg  6233  elmpt2cl  6291  1st2val  6375  2nd2val  6376  bropopvvv  6429  ovmptss  6431  oprab2co  6435  curry1  6441  curry2  6444  algrflem  6458  mpt2xopn0yelv  6467  mpt2xopxnop0  6469  ovtpos  6497  seqomlem1  6710  seqomlem4  6713  brwitnlem  6754  cantnfvalf  7623  fseqenlem1  7910  axdc4lem  8340  fpwwe  8526  canthwelem  8530  addpiord  8766  mulpiord  8767  addpqnq  8820  mulpqnq  8823  recmulnq  8846  dmrecnq  8850  cnref1o  10612  ixxssxr  10933  om2uzrdg  11301  uzrdgsuci  11305  swrd00  11770  cnrecnv  11975  sadcf  12970  smupf  12995  eucalgval  13078  eucalginv  13080  eucalglt  13081  eucalg  13083  vdwmc  13351  isstruct2  13483  isstruct  13484  imasaddvallem  13759  imasvscafn  13767  imasvscaval  13768  xpsff1o  13798  xpsaddlem  13805  xpsvsca  13809  xpsle  13811  comffval  13930  comfffval2  13932  comfeq  13937  isoval  13995  isssc  14025  isfuncd  14067  funcf2  14070  idfu2nd  14079  idfucl  14083  cofucl  14090  resfval2  14095  resf2nd  14097  funcres2b  14099  funcpropd  14102  homarcl  14188  homaval  14191  homarcl2  14195  arwhoma  14205  coapm  14231  catcco  14261  catcisolem  14266  xpcco  14285  xpcid  14291  xpcpropd  14310  evlfcllem  14323  evlfcl  14324  curf1cl  14330  curf2cl  14333  curfcl  14334  uncf1  14338  uncf2  14339  uncfcurf  14341  diag11  14345  diag12  14346  diag2  14347  curf2ndf  14349  hof2fval  14357  hofcl  14361  hofpropd  14369  yonedalem21  14375  yonedalem22  14380  yonedalem3b  14381  yonedalem3  14382  yonedainv  14383  yonffthlem  14384  plusffval  14707  gaid  15081  oppglsm  15281  efgmnvl  15351  efgval2  15361  vrgpinv  15406  frgpuptinv  15408  frgpuplem  15409  frgpup2  15413  frgpup3lem  15414  frgpnabllem1  15489  gsum2d  15551  gsum2d2lem  15552  gsumcom2  15554  eldprd  15567  dprd2dlem2  15603  dprd2dlem1  15604  dprd2da  15605  scaffval  15973  ipffval  16884  iccordt  17283  iscnp2  17308  ptbasfi  17618  txcnpi  17645  txdis1cn  17672  lmcn2  17686  xkococn  17697  cnmpt12f  17703  cnmpt21  17708  cnmpt2t  17710  cnmpt22  17711  cnmpt2k  17725  xkohmeo  17852  flfcnp2  18044  tmdcn2  18124  clssubg  18143  tgphaus  18151  divstgplem  18155  psmetxrge0  18349  imasdsf1olem  18408  xpsdsval  18416  xmeterval  18467  comet  18548  txmetcnp  18582  metustidOLD  18594  metustid  18595  metustsymOLD  18596  metustsym  18597  metustexhalfOLD  18598  metustexhalf  18599  blval2  18610  metuel2  18614  nrmmetd  18627  nmfval  18641  isngp3  18650  ngpds  18655  tngnm  18697  qtopbaslem  18797  cnmetdval  18810  remetdval  18825  tgqioo  18836  bndth  18988  htpyco2  19009  phtpyco2  19020  caubl  19265  caublcls  19266  bcthlem1  19282  bcthlem2  19283  bcthlem4  19285  bcthlem5  19286  ovolfioo  19369  ovolficc  19370  ovolficcss  19371  ovolfsval  19372  ovolctb  19391  ovoliunlem2  19404  ovolicc2lem1  19418  ovolicc2lem5  19422  ovolfs2  19468  ioorinv  19473  uniiccdif  19475  uniioovol  19476  uniiccvol  19477  uniioombllem2a  19479  uniioombllem2  19480  uniioombllem3a  19481  uniioombllem3  19482  uniioombllem4  19483  uniioombllem5  19484  uniioombllem6  19485  dyadovol  19490  dyadss  19491  dyaddisjlem  19492  dyadmaxlem  19494  dyadmbl  19497  opnmbllem  19498  itg1addlem4  19594  limccnp2  19784  dvbsss  19794  perfdvf  19795  dvdsmulf1o  20984  fsumdvdsmul  20985  fsumvma  21002  grposn  21808  rngosn  21997  imsdval  22183  elovimad  24056  ofresid  24060  ofoprabco  24084  xrofsup  24131  logb2aval  24396  elunirnmbfm  24608  sibfof  24659  cndprobval  24696  cvmlift2lem9  25003  cvmlift2lem10  25004  cvmlift2lem13  25007  cvmliftphtlem  25009  fvtransport  25971  fvray  26080  linedegen  26082  fvline  26083  opnmbllem0  26254  mblfinlem1  26255  mblfinlem2  26256  ftc1anc  26302  ftc2nc  26303  opropabco  26439  f1opr  26440  ismtyhmeolem  26527  heiborlem3  26536  heiborlem4  26537  heiborlem6  26539  heiborlem8  26541  mamudi  27452  mamudir  27453  mamuvs1  27454  mamuvs2  27455  aovfundmoveq  28035  aovpcov0  28044  aovnuoveq  28045  aovvoveq  28046  aov0ov0  28047  aovovn0oveq  28048  aov0nbovbi  28049  aovov0bi  28050  2wlkonot3v  28407  2spthonot3v  28408
  Copyright terms: Public domain W3C validator