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

Definition df-ov 6366
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 𝐹 and its arguments 𝐴 and 𝐵- will be useful for proving meaningful theorems. For example, if class 𝐹 is the operation + and arguments 𝐴 and 𝐵 are 3 and 2, the expression (3 + 2) can be proved to equal 5 (see 3p2e5 10832). This definition is well-defined, although not very meaningful, when classes 𝐴 and/or 𝐵 are proper classes (i.e. are not sets); see ovprc1 6395 and ovprc2 6396. On the other hand, we often find uses for this definition when 𝐹 is a proper class, such as +𝑜 in oav 7290. 𝐹 is normally equal to a class of nested ordered pairs of the form defined by df-oprab 6367. (Contributed by NM, 28-Feb-1995.)
Assertion
Ref Expression
df-ov (𝐴𝐹𝐵) = (𝐹‘⟨𝐴, 𝐵⟩)

Detailed syntax breakdown of Definition df-ov
StepHypRef Expression
1 cA . . 3 class 𝐴
2 cB . . 3 class 𝐵
3 cF . . 3 class 𝐹
41, 2, 3co 6363 . 2 class (𝐴𝐹𝐵)
51, 2cop 4001 . . 3 class 𝐴, 𝐵
65, 3cfv 5633 . 2 class (𝐹‘⟨𝐴, 𝐵⟩)
74, 6wceq 1468 1 wff (𝐴𝐹𝐵) = (𝐹‘⟨𝐴, 𝐵⟩)
Colors of variables: wff setvar class
This definition is referenced by:  oveq  6369  oveq1  6370  oveq2  6371  nfovd  6388  ovex  6391  ovssunirn  6392  0ov  6393  ovprc  6394  csbov123  6398  csbov  6399  elovimad  6404  fnotovb  6405  ffnov  6475  eqfnov  6477  fnov  6479  ovid  6488  ovidig  6489  ov  6491  ovigg  6492  ov6g  6509  ovg  6510  ovres  6511  fovrn  6514  fnrnov  6517  foov  6518  fnovrn  6519  funimassov  6521  ovelimab  6522  ovima0  6523  ovconst2  6524  oprssdm  6525  nssdmovg  6526  ndmovg  6527  elmpt2cl  6586  1st2val  6896  2nd2val  6897  brovpreldm  6952  bropopvvv  6953  bropfvvvvlem  6954  ovmptss  6956  oprab2co  6960  curry1  6967  curry2  6970  algrflem  6984  mpt2xeldm  7035  mpt2xopn0yelv  7037  mpt2xopxnop0  7039  ovtpos  7065  mpt2curryd  7093  seqomlem1  7244  seqomlem4  7247  brwitnlem  7286  cantnfvalf  8255  fseqenlem1  8540  axdc4lem  8970  fpwwe  9156  canthwelem  9160  addpiord  9394  mulpiord  9395  addpqnq  9448  mulpqnq  9451  recmulnq  9474  dmrecnq  9478  cnref1o  11388  ixxssxr  11742  om2uzrdg  12283  uzrdgsuci  12287  swrd00  12908  swrd0  12924  cnrecnv  13388  sadcf  14589  smupf  14614  eucalgval  14703  eucalginv  14705  eucalglt  14706  eucalg  14708  vdwmc  15090  isstruct2  15291  isstruct  15292  imasaddvallem  15600  imasvscafn  15608  imasvscaval  15609  xpsff1o  15639  xpsaddlem  15646  xpsvsca  15650  xpsle  15652  comffval  15770  comfffval2  15772  comfeq  15777  isoval  15836  brcic  15869  isssc  15891  isfuncd  15936  funcf2  15939  idfu2nd  15948  idfucl  15952  cofucl  15959  resfval2  15964  resf2nd  15966  funcres2b  15968  funcpropd  15971  homaval  16092  homarcl2  16096  arwhoma  16106  coapm  16132  catcco  16162  catcisolem  16167  xpcco  16234  xpcid  16240  xpcpropd  16259  evlfcllem  16272  evlfcl  16273  curf1cl  16279  curf2cl  16282  curfcl  16283  uncf1  16287  uncf2  16288  uncfcurf  16290  diag11  16294  diag12  16295  diag2  16296  curf2ndf  16298  hof2fval  16306  hofcl  16310  hofpropd  16318  yonedalem21  16324  yonedalem22  16329  yonedalem3b  16330  yonedalem3  16331  yonedainv  16332  yonffthlem  16333  joinval  16416  meetval  16430  plusffval  16658  mgm1  16665  sgrp1  16699  mnd1  16738  mnd1id  16739  grp1  16918  gaid  17114  efgmnvl  17525  efgval2  17535  vrgpinv  17580  frgpuptinv  17582  frgpuplem  17583  frgpup2  17587  frgpup3lem  17588  frgpnabllem1  17670  gsum2dlem1  17763  gsum2dlem2  17764  gsum2d  17765  gsum2d2lem  17766  gsumcom2  17768  eldprd  17797  dprd2dlem2  17833  dprd2dlem1  17834  dprd2da  17835  ring1  17990  scaffval  18269  ply1frcl  19065  ipffval  19373  mamudi  19586  mamudir  19587  mamuvs1  19588  mamuvs2  19589  matplusgcell  19616  matsubgcell  19617  matvscacell  19619  mat1dimmul  19659  mat1rhmelval  19663  mdetrlin  19785  mdetrsca  19786  pmatcoe1fsupp  19883  iccordt  20387  iscnp2  20412  ptbasfi  20753  txcnpi  20780  txdis1cn  20807  lmcn2  20821  xkococn  20832  cnmpt12f  20838  cnmpt21  20843  cnmpt2t  20845  cnmpt22  20846  cnmpt2k  20860  xkohmeo  20987  flfcnp2  21180  tmdcn2  21262  clssubg  21281  tgphaus  21289  qustgplem  21293  psmetxrge0  21487  imasdsf1olem  21546  xpsdsval  21554  xmeterval  21605  comet  21686  txmetcnp  21720  metustid  21727  metustsym  21728  metustexhalf  21729  blval2  21735  metuel2  21738  nrmmetd  21747  nmfval  21761  isngp3  21770  ngpds  21775  tngnm  21817  qtopbaslem  21937  cnmetdval  21949  remetdval  21965  tgqioo  21976  bndth  22144  htpyco2  22168  phtpyco2  22179  caubl  22436  caublcls  22437  bcthlem1  22451  bcthlem2  22452  bcthlem4  22454  bcthlem5  22455  ovolfioo  22579  ovolficc  22580  ovolficcss  22581  ovolfsval  22582  ovolctb  22602  ovoliunlem2  22615  ovolicc2lem1  22629  ovolicc2lem5  22634  ovolfs2  22683  ioorinv  22688  ioorinvOLD  22693  uniiccdif  22695  uniioovol  22696  uniiccvol  22697  uniioombllem2a  22699  uniioombllem2  22700  uniioombllem2OLD  22701  uniioombllem3a  22702  uniioombllem3  22703  uniioombllem4  22704  uniioombllem5  22705  uniioombllem6  22706  dyadovol  22711  dyadss  22712  dyaddisjlem  22713  dyadmaxlem  22715  dyadmbl  22718  opnmbllem  22719  itg1addlem4  22818  limccnp2  23008  dvbsss  23018  perfdvf  23019  dvdsmulf1o  24284  fsumdvdsmul  24285  fsumvma  24302  tglngne  24756  ltgseg  24802  tgelrnln  24836  edgov  25229  usgraexmplvtx  25291  usgraexmplcvtx  25294  usgraexmplcedg  25295  2wlkonot3v  25763  2spthonot3v  25764  isrgrac  25822  grposn  26106  rngosn  26295  imsdval  26481  ofresid  28401  ofoprabco  28424  xrofsup  28509  smatrcl  28777  smatlem  28778  fvproj  28814  elunirnmbfm  29229  sibfof  29327  oddpwdcv  29342  eulerpartlemgh  29365  cndprobval  29420  cvmlift2lem9  30186  cvmlift2lem10  30187  cvmlift2lem13  30190  cvmliftphtlem  30192  fvtransport  30950  fvray  31059  linedegen  31061  fvline  31062  bj-finsumval0  31923  icoreunrn  31983  relowlpssretop  31988  finxpreclem1  32002  finxpreclem2  32003  finxpreclem3  32006  finxpreclem5  32008  curfv  32158  uncov  32159  curunc  32160  opnmbllem0  32214  mblfinlem1  32215  mblfinlem2  32216  ftc1anc  32263  ftc2nc  32264  opropabco  32288  f1opr  32289  ismtyhmeolem  32373  heiborlem3  32382  heiborlem4  32383  heiborlem6  32385  heiborlem8  32387  fvovco  37829  volioof  38284  fvvolioof  38286  fvvolicof  38288  fourierdlem42  38448  fourierdlem42OLD  38449  hoi2toco  38892  ovolval2lem  38928  ovolval3  38932  ovolval4lem1  38934  ovolval5lem2  38938  ovnovollem1  38941  ovnovollem2  38942  aovfundmoveq  39203  aovpcov0  39212  aovnuoveq  39213  aovvoveq  39214  aov0ov0  39215  aovovn0oveq  39216  aov0nbovbi  39217  aovov0bi  39218  pfx00  39447  pfx0  39448  opvtxov  39638  opiedgov  39641  edgaov  39755  ovn0dmfun  40954  ovn0ssdmfun  40957  plusfreseq  40962  idfusubc0  41055  rhmsubclem2  41279  rhmsubcALTVlem2  41298  lmod1lem2  41471  lmod1lem3  41472  logb2aval  41681
  Copyright terms: Public domain W3C validator