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

Definition df-ov 6199
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 10585). 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 6227 and ovprc2 6228. On the other hand, we often find uses for this definition when  F is a proper class, such as  +o in oav 7079.  F is normally equal to a class of nested ordered pairs of the form defined by df-oprab 6200. (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 6196 . 2  class  ( A F B )
51, 2cop 3950 . . 3  class  <. A ,  B >.
65, 3cfv 5496 . 2  class  ( F `
 <. A ,  B >. )
74, 6wceq 1399 1  wff  ( A F B )  =  ( F `  <. A ,  B >. )
Colors of variables: wff setvar class
This definition is referenced by:  oveq  6202  oveq1  6203  oveq2  6204  nfovd  6221  ovex  6224  ovssunirn  6225  ovprc  6226  csbov123  6230  csbov  6231  elovimad  6236  fnotovb  6237  ffnov  6305  eqfnov  6307  fnov  6309  ovid  6318  ovidig  6319  ov  6321  ovigg  6322  ov6g  6339  ovg  6340  ovres  6341  fovrn  6344  fnrnov  6347  foov  6348  fnovrn  6349  funimassov  6351  ovelimab  6352  ovima0  6353  ovconst2  6354  oprssdm  6355  nssdmovg  6356  ndmovg  6357  elmpt2cl  6416  1st2val  6725  2nd2val  6726  bropopvvv  6779  ovmptss  6780  oprab2co  6784  curry1  6791  curry2  6794  algrflem  6808  mpt2xopn0yelv  6859  mpt2xopxnop0  6861  ovtpos  6888  mpt2curryd  6916  seqomlem1  7033  seqomlem4  7036  brwitnlem  7075  cantnfvalf  7997  fseqenlem1  8318  axdc4lem  8748  fpwwe  8935  canthwelem  8939  addpiord  9173  mulpiord  9174  addpqnq  9227  mulpqnq  9230  recmulnq  9253  dmrecnq  9257  cnref1o  11134  ixxssxr  11462  om2uzrdg  11970  uzrdgsuci  11974  swrd00  12554  swrd0  12570  cnrecnv  13000  sadcf  14105  smupf  14130  eucalgval  14213  eucalginv  14215  eucalglt  14216  eucalg  14218  vdwmc  14498  isstruct2  14643  isstruct  14644  imasaddvallem  14936  imasvscafn  14944  imasvscaval  14945  xpsff1o  14975  xpsaddlem  14982  xpsvsca  14986  xpsle  14988  comffval  15105  comfffval2  15107  comfeq  15112  isoval  15171  brcic  15204  isssc  15226  isfuncd  15271  funcf2  15274  idfu2nd  15283  idfucl  15287  cofucl  15294  resfval2  15299  resf2nd  15301  funcres2b  15303  funcpropd  15306  homarcl  15424  homaval  15427  homarcl2  15431  arwhoma  15441  coapm  15467  catcco  15497  catcisolem  15502  xpcco  15569  xpcid  15575  xpcpropd  15594  evlfcllem  15607  evlfcl  15608  curf1cl  15614  curf2cl  15617  curfcl  15618  uncf1  15622  uncf2  15623  uncfcurf  15625  diag11  15629  diag12  15630  diag2  15631  curf2ndf  15633  hof2fval  15641  hofcl  15645  hofpropd  15653  yonedalem21  15659  yonedalem22  15664  yonedalem3b  15665  yonedalem3  15666  yonedainv  15667  yonffthlem  15668  joinval  15752  meetval  15766  plusffval  15994  mgm1  16001  sgrp1  16035  mnd1  16078  mnd1OLD  16079  mnd1id  16080  grp1  16259  gaid  16454  oppglsm  16779  efgmnvl  16849  efgval2  16859  vrgpinv  16904  frgpuptinv  16906  frgpuplem  16907  frgpup2  16911  frgpup3lem  16912  frgpnabllem1  16994  gsum2dlem1  17111  gsum2dlem2  17112  gsum2d  17113  gsum2dOLD  17114  gsum2d2lem  17115  gsumcom2  17117  eldprd  17148  eldprdOLD  17150  dprd2dlem2  17202  dprd2dlem1  17203  dprd2da  17204  ring1  17361  scaffval  17643  ply1frcl  18468  ipffval  18774  mamudi  18990  mamudir  18991  mamuvs1  18992  mamuvs2  18993  matplusgcell  19020  matsubgcell  19021  matvscacell  19023  mat1dimmul  19063  mat1rhmelval  19067  mdetrlin  19189  mdetrsca  19190  pmatcoe1fsupp  19287  iccordt  19801  iscnp2  19826  ptbasfi  20167  txcnpi  20194  txdis1cn  20221  lmcn2  20235  xkococn  20246  cnmpt12f  20252  cnmpt21  20257  cnmpt2t  20259  cnmpt22  20260  cnmpt2k  20274  xkohmeo  20401  flfcnp2  20593  tmdcn2  20673  clssubg  20692  tgphaus  20700  qustgplem  20704  psmetxrge0  20902  imasdsf1olem  20961  xpsdsval  20969  xmeterval  21020  comet  21101  txmetcnp  21135  metustidOLD  21147  metustid  21148  metustsymOLD  21149  metustsym  21150  metustexhalfOLD  21151  metustexhalf  21152  blval2  21163  metuel2  21167  nrmmetd  21180  nmfval  21194  isngp3  21203  ngpds  21208  tngnm  21250  qtopbaslem  21350  cnmetdval  21363  remetdval  21379  tgqioo  21390  bndth  21543  htpyco2  21564  phtpyco2  21575  caubl  21831  caublcls  21832  bcthlem1  21848  bcthlem2  21849  bcthlem4  21851  bcthlem5  21852  ovolfioo  21964  ovolficc  21965  ovolficcss  21966  ovolfsval  21967  ovolctb  21986  ovoliunlem2  21999  ovolicc2lem1  22013  ovolicc2lem5  22017  ovolfs2  22065  ioorinv  22070  uniiccdif  22072  uniioovol  22073  uniiccvol  22074  uniioombllem2a  22076  uniioombllem2  22077  uniioombllem3a  22078  uniioombllem3  22079  uniioombllem4  22080  uniioombllem5  22081  uniioombllem6  22082  dyadovol  22087  dyadss  22088  dyaddisjlem  22089  dyadmaxlem  22091  dyadmbl  22094  opnmbllem  22095  itg1addlem4  22191  limccnp2  22381  dvbsss  22391  perfdvf  22392  dvdsmulf1o  23587  fsumdvdsmul  23588  fsumvma  23605  tglngne  24057  ltgseg  24102  tgelrnln  24130  edgov  24462  usgraexmplvtx  24523  usgraexmplcvtx  24526  usgraexmplcedg  24527  2wlkonot3v  24996  2spthonot3v  24997  isrgrac  25055  grposn  25334  rngosn  25523  imsdval  25709  ofresid  27622  ofoprabco  27651  xrofsup  27735  fvproj  27989  elunirnmbfm  28380  sibfof  28465  oddpwdcv  28477  eulerpartlemgh  28500  cndprobval  28555  cvmlift2lem9  28945  cvmlift2lem10  28946  cvmlift2lem13  28949  cvmliftphtlem  28951  mclsrcl  29110  fvtransport  29835  fvray  29944  linedegen  29946  fvline  29947  opnmbllem0  30215  mblfinlem1  30216  mblfinlem2  30217  ftc1anc  30264  ftc2nc  30265  opropabco  30380  f1opr  30381  ismtyhmeolem  30466  heiborlem3  30475  heiborlem4  30476  heiborlem6  30478  heiborlem8  30480  fourierdlem42  32097  aovfundmoveq  32432  aovpcov0  32441  aovnuoveq  32442  aovvoveq  32443  aov0ov0  32444  aovovn0oveq  32445  aov0nbovbi  32446  aovov0bi  32447  pfx00  32559  pfx0  32560  uhgrasize  32711  usgrafisbaseALT  32758  usgrafisbaseALT2  32759  usgfis  32764  usgfisALT  32768  ovn0dmfun  32770  ovn0ssdmfun  32773  plusfreseq  32778  idfusubc0  32871  rhmsubclem2  33095  rhmsubcALTVlem2  33114  lmod1lem2  33289  lmod1lem3  33290  logb2aval  33503  bj-finsumval0  35010
  Copyright terms: Public domain W3C validator