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

Definition df-ov 6308
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 10742). 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 6336 and ovprc2 6337. On the other hand, we often find uses for this definition when  F is a proper class, such as  +o in oav 7221.  F is normally equal to a class of nested ordered pairs of the form defined by df-oprab 6309. (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 6305 . 2  class  ( A F B )
51, 2cop 4008 . . 3  class  <. A ,  B >.
65, 3cfv 5601 . 2  class  ( F `
 <. A ,  B >. )
74, 6wceq 1437 1  wff  ( A F B )  =  ( F `  <. A ,  B >. )
Colors of variables: wff setvar class
This definition is referenced by:  oveq  6311  oveq1  6312  oveq2  6313  nfovd  6330  ovex  6333  ovssunirn  6334  ovprc  6335  csbov123  6339  csbov  6340  elovimad  6345  fnotovb  6346  ffnov  6414  eqfnov  6416  fnov  6418  ovid  6427  ovidig  6428  ov  6430  ovigg  6431  ov6g  6448  ovg  6449  ovres  6450  fovrn  6453  fnrnov  6456  foov  6457  fnovrn  6458  funimassov  6460  ovelimab  6461  ovima0  6462  ovconst2  6463  oprssdm  6464  nssdmovg  6465  ndmovg  6466  elmpt2cl  6525  1st2val  6833  2nd2val  6834  bropopvvv  6887  ovmptss  6888  oprab2co  6892  curry1  6899  curry2  6902  algrflem  6916  mpt2xopn0yelv  6967  mpt2xopxnop0  6969  ovtpos  6996  mpt2curryd  7024  seqomlem1  7175  seqomlem4  7178  brwitnlem  7217  cantnfvalf  8169  fseqenlem1  8453  axdc4lem  8883  fpwwe  9070  canthwelem  9074  addpiord  9308  mulpiord  9309  addpqnq  9362  mulpqnq  9365  recmulnq  9388  dmrecnq  9392  cnref1o  11297  ixxssxr  11647  om2uzrdg  12167  uzrdgsuci  12171  swrd00  12759  swrd0  12775  cnrecnv  13207  sadcf  14401  smupf  14426  eucalgval  14512  eucalginv  14514  eucalglt  14515  eucalg  14517  vdwmc  14891  isstruct2  15093  isstruct  15094  imasaddvallem  15386  imasvscafn  15394  imasvscaval  15395  xpsff1o  15425  xpsaddlem  15432  xpsvsca  15436  xpsle  15438  comffval  15555  comfffval2  15557  comfeq  15562  isoval  15621  brcic  15654  isssc  15676  isfuncd  15721  funcf2  15724  idfu2nd  15733  idfucl  15737  cofucl  15744  resfval2  15749  resf2nd  15751  funcres2b  15753  funcpropd  15756  homarcl  15874  homaval  15877  homarcl2  15881  arwhoma  15891  coapm  15917  catcco  15947  catcisolem  15952  xpcco  16019  xpcid  16025  xpcpropd  16044  evlfcllem  16057  evlfcl  16058  curf1cl  16064  curf2cl  16067  curfcl  16068  uncf1  16072  uncf2  16073  uncfcurf  16075  diag11  16079  diag12  16080  diag2  16081  curf2ndf  16083  hof2fval  16091  hofcl  16095  hofpropd  16103  yonedalem21  16109  yonedalem22  16114  yonedalem3b  16115  yonedalem3  16116  yonedainv  16117  yonffthlem  16118  joinval  16202  meetval  16216  plusffval  16444  mgm1  16451  sgrp1  16485  mnd1  16528  mnd1OLD  16529  mnd1id  16530  grp1  16709  gaid  16904  oppglsm  17229  efgmnvl  17299  efgval2  17309  vrgpinv  17354  frgpuptinv  17356  frgpuplem  17357  frgpup2  17361  frgpup3lem  17362  frgpnabllem1  17444  gsum2dlem1  17537  gsum2dlem2  17538  gsum2d  17539  gsum2d2lem  17540  gsumcom2  17542  eldprd  17571  dprd2dlem2  17608  dprd2dlem1  17609  dprd2da  17610  ring1  17765  scaffval  18044  ply1frcl  18842  ipffval  19146  mamudi  19359  mamudir  19360  mamuvs1  19361  mamuvs2  19362  matplusgcell  19389  matsubgcell  19390  matvscacell  19392  mat1dimmul  19432  mat1rhmelval  19436  mdetrlin  19558  mdetrsca  19559  pmatcoe1fsupp  19656  iccordt  20161  iscnp2  20186  ptbasfi  20527  txcnpi  20554  txdis1cn  20581  lmcn2  20595  xkococn  20606  cnmpt12f  20612  cnmpt21  20617  cnmpt2t  20619  cnmpt22  20620  cnmpt2k  20634  xkohmeo  20761  flfcnp2  20953  tmdcn2  21035  clssubg  21054  tgphaus  21062  qustgplem  21066  psmetxrge0  21260  imasdsf1olem  21319  xpsdsval  21327  xmeterval  21378  comet  21459  txmetcnp  21493  metustid  21500  metustsym  21501  metustexhalf  21502  blval2  21508  metuel2  21511  nrmmetd  21520  nmfval  21534  isngp3  21543  ngpds  21548  tngnm  21590  qtopbaslem  21690  cnmetdval  21702  remetdval  21718  tgqioo  21729  bndth  21882  htpyco2  21903  phtpyco2  21914  caubl  22170  caublcls  22171  bcthlem1  22185  bcthlem2  22186  bcthlem4  22188  bcthlem5  22189  ovolfioo  22299  ovolficc  22300  ovolficcss  22301  ovolfsval  22302  ovolctb  22321  ovoliunlem2  22334  ovolicc2lem1  22348  ovolicc2lem5  22352  ovolfs2  22400  ioorinv  22405  ioorinvOLD  22410  uniiccdif  22412  uniioovol  22413  uniiccvol  22414  uniioombllem2a  22416  uniioombllem2  22417  uniioombllem2OLD  22418  uniioombllem3a  22419  uniioombllem3  22420  uniioombllem4  22421  uniioombllem5  22422  uniioombllem6  22423  dyadovol  22428  dyadss  22429  dyaddisjlem  22430  dyadmaxlem  22432  dyadmbl  22435  opnmbllem  22436  itg1addlem4  22534  limccnp2  22724  dvbsss  22734  perfdvf  22735  dvdsmulf1o  23986  fsumdvdsmul  23987  fsumvma  24004  tglngne  24455  ltgseg  24501  tgelrnln  24534  edgov  24914  usgraexmplvtx  24975  usgraexmplcvtx  24978  usgraexmplcedg  24979  2wlkonot3v  25448  2spthonot3v  25449  isrgrac  25507  grposn  25788  rngosn  25977  imsdval  26163  ofresid  28083  ofoprabco  28107  xrofsup  28189  smatrcl  28461  smatlem  28462  fvproj  28498  elunirnmbfm  28914  sibfof  29001  oddpwdcv  29014  eulerpartlemgh  29037  cndprobval  29092  cvmlift2lem9  29822  cvmlift2lem10  29823  cvmlift2lem13  29826  cvmliftphtlem  29828  mclsrcl  29987  fvtransport  30584  fvray  30693  linedegen  30695  fvline  30696  bj-finsumval0  31447  icoreunrn  31496  relowlpssretop  31501  opnmbllem0  31679  mblfinlem1  31680  mblfinlem2  31681  ftc1anc  31728  ftc2nc  31729  opropabco  31753  f1opr  31754  ismtyhmeolem  31839  heiborlem3  31848  heiborlem4  31849  heiborlem6  31851  heiborlem8  31853  fourierdlem42  37579  aovfundmoveq  38072  aovpcov0  38081  aovnuoveq  38082  aovvoveq  38083  aov0ov0  38084  aovovn0oveq  38085  aov0nbovbi  38086  aovov0bi  38087  pfx00  38314  pfx0  38315  uhgrasize  38462  usgrafisbaseALT  38509  usgrafisbaseALT2  38510  usgfis  38515  usgfisALT  38519  ovn0dmfun  38521  ovn0ssdmfun  38524  plusfreseq  38529  idfusubc0  38622  rhmsubclem2  38846  rhmsubcALTVlem2  38865  lmod1lem2  39040  lmod1lem3  39041  logb2aval  39253
  Copyright terms: Public domain W3C validator