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 6607
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 11104). This definition is well-defined, although not very meaningful, when classes 𝐴 and/or 𝐵 are proper classes (i.e. are not sets); see ovprc1 6637 and ovprc2 6638. On the other hand, we often find uses for this definition when 𝐹 is a proper class, such as +𝑜 in oav 7536. 𝐹 is normally equal to a class of nested ordered pairs of the form defined by df-oprab 6608. (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 6604 . 2 class (𝐴𝐹𝐵)
51, 2cop 4154 . . 3 class 𝐴, 𝐵
65, 3cfv 5847 . 2 class (𝐹‘⟨𝐴, 𝐵⟩)
74, 6wceq 1480 1 wff (𝐴𝐹𝐵) = (𝐹‘⟨𝐴, 𝐵⟩)
Colors of variables: wff setvar class
This definition is referenced by:  oveq  6610  oveq1  6611  oveq2  6612  nfovd  6629  ovex  6632  ovssunirn  6634  0ov  6635  ovprc  6636  csbov123  6640  csbov  6641  elovimad  6646  fnotovb  6647  ffnov  6717  eqfnov  6719  fnov  6721  ovid  6730  ovidig  6731  ov  6733  ovigg  6734  ov6g  6751  ovg  6752  ovres  6753  fovrn  6757  fnrnov  6760  foov  6761  fnovrn  6762  funimassov  6764  ovelimab  6765  ovima0  6766  ovconst2  6767  oprssdm  6768  nssdmovg  6769  ndmovg  6770  elmpt2cl  6829  1st2val  7139  2nd2val  7140  brovpreldm  7199  bropopvvv  7200  bropfvvvvlem  7201  ovmptss  7203  oprab2co  7207  curry1  7214  curry2  7217  algrflem  7231  mpt2xeldm  7282  mpt2xopn0yelv  7284  mpt2xopxnop0  7286  ovtpos  7312  mpt2curryd  7340  seqomlem1  7490  seqomlem4  7493  brwitnlem  7532  cantnfvalf  8506  fseqenlem1  8791  axdc4lem  9221  fpwwe  9412  canthwelem  9416  addpiord  9650  mulpiord  9651  addpqnq  9704  mulpqnq  9707  recmulnq  9730  dmrecnq  9734  cnref1o  11771  ixxssxr  12129  om2uzrdg  12695  uzrdgsuci  12699  swrd00  13356  swrd0  13372  cnrecnv  13839  sadcf  15099  smupf  15124  eucalgval  15219  eucalginv  15221  eucalglt  15222  eucalg  15224  vdwmc  15606  isstruct2  15790  isstruct  15793  setsstruct2  15817  imasaddvallem  16110  imasvscafn  16118  imasvscaval  16119  xpsff1o  16149  xpsaddlem  16156  xpsvsca  16160  xpsle  16162  comffval  16280  comfffval2  16282  comfeq  16287  isoval  16346  brcic  16379  isssc  16401  isfuncd  16446  funcf2  16449  idfu2nd  16458  idfucl  16462  cofucl  16469  resfval2  16474  resf2nd  16476  funcres2b  16478  funcpropd  16481  homaval  16602  homarcl2  16606  arwhoma  16616  coapm  16642  catcco  16672  catcisolem  16677  xpcco  16744  xpcid  16750  xpcpropd  16769  evlfcllem  16782  evlfcl  16783  curf1cl  16789  curf2cl  16792  curfcl  16793  uncf1  16797  uncf2  16798  uncfcurf  16800  diag11  16804  diag12  16805  diag2  16806  curf2ndf  16808  hof2fval  16816  hofcl  16820  hofpropd  16828  yonedalem21  16834  yonedalem22  16839  yonedalem3b  16840  yonedalem3  16841  yonedainv  16842  yonffthlem  16843  joinval  16926  meetval  16940  plusffval  17168  mgm1  17178  sgrp1  17214  mnd1  17252  mnd1id  17253  grp1  17443  gaid  17653  efgmnvl  18048  efgval2  18058  vrgpinv  18103  frgpuptinv  18105  frgpuplem  18106  frgpup2  18110  frgpup3lem  18111  frgpnabllem1  18197  gsum2dlem1  18290  gsum2dlem2  18291  gsum2d  18292  gsum2d2lem  18293  gsumcom2  18295  eldprd  18324  dprd2dlem2  18360  dprd2dlem1  18361  dprd2da  18362  srgfcl  18436  ring1  18523  scaffval  18802  ply1frcl  19602  ipffval  19912  mamudi  20128  mamudir  20129  mamuvs1  20130  mamuvs2  20131  matplusgcell  20158  matsubgcell  20159  matvscacell  20161  mat1dimmul  20201  mat1rhmelval  20205  mdetrlin  20327  mdetrsca  20328  pmatcoe1fsupp  20425  iccordt  20928  iscnp2  20953  ptbasfi  21294  txcnpi  21321  txdis1cn  21348  lmcn2  21362  xkococn  21373  cnmpt12f  21379  cnmpt21  21384  cnmpt2t  21386  cnmpt22  21387  cnmpt2k  21401  xkohmeo  21528  flfcnp2  21721  tmdcn2  21803  clssubg  21822  tgphaus  21830  qustgplem  21834  psmetxrge0  22028  imasdsf1olem  22088  xpsdsval  22096  xmeterval  22147  comet  22228  txmetcnp  22262  metustid  22269  metustsym  22270  metustexhalf  22271  blval2  22277  metuel2  22280  nrmmetd  22289  nmfval  22303  isngp3  22312  ngpds  22318  tngnm  22365  qtopbaslem  22472  cnmetdval  22484  remetdval  22500  tgqioo  22511  bndth  22665  htpyco2  22686  phtpyco2  22697  caubl  23014  caublcls  23015  bcthlem1  23029  bcthlem2  23030  bcthlem4  23032  bcthlem5  23033  ovolfioo  23143  ovolficc  23144  ovolficcss  23145  ovolfsval  23146  ovolctb  23165  ovoliunlem2  23178  ovolicc2lem1  23192  ovolicc2lem5  23196  ovolfs2  23245  ioorinv  23250  uniiccdif  23252  uniioovol  23253  uniiccvol  23254  uniioombllem2a  23256  uniioombllem2  23257  uniioombllem3a  23258  uniioombllem3  23259  uniioombllem4  23260  uniioombllem5  23261  uniioombllem6  23262  dyadovol  23267  dyadss  23268  dyaddisjlem  23269  dyadmaxlem  23271  dyadmbl  23274  opnmbllem  23275  itg1addlem4  23372  limccnp2  23562  dvbsss  23572  perfdvf  23573  dvdsmulf1o  24820  fsumdvdsmul  24821  fsumvma  24838  tglngne  25345  ltgseg  25391  tgelrnln  25425  opvtxov  25785  opiedgov  25788  edgov  25843  imsdval  27387  ofresid  29283  ofoprabco  29304  xrofsup  29374  smatrcl  29641  smatlem  29642  fvproj  29678  elunirnmbfm  30093  sibfof  30180  oddpwdcv  30195  eulerpartlemgh  30218  cndprobval  30273  cvmlift2lem9  30998  cvmlift2lem10  30999  cvmlift2lem13  31002  cvmliftphtlem  31004  fvtransport  31778  fvray  31887  linedegen  31889  fvline  31890  bj-finsumval0  32777  icoreunrn  32836  relowlpssretop  32841  finxpreclem1  32855  finxpreclem2  32856  finxpreclem3  32859  finxpreclem5  32861  curfv  33018  uncov  33019  curunc  33020  opnmbllem0  33074  mblfinlem1  33075  mblfinlem2  33076  ftc1anc  33122  ftc2nc  33123  opropabco  33147  f1opr  33148  ismtyhmeolem  33232  heiborlem3  33241  heiborlem4  33242  heiborlem6  33244  heiborlem8  33246  grposnOLD  33310  fvovco  38852  volioof  39508  fvvolioof  39510  fvvolicof  39512  fourierdlem42  39670  hoi2toco  40125  ovolval2lem  40161  ovolval3  40165  ovolval4lem1  40167  ovolval5lem2  40171  ovnovollem1  40174  ovnovollem2  40175  smfpimbor1lem1  40309  aovfundmoveq  40562  aovpcov0  40571  aovnuoveq  40572  aovvoveq  40573  aov0ov0  40574  aovovn0oveq  40575  aov0nbovbi  40576  aovov0bi  40577  pfx00  40680  pfx0  40681  ovn0dmfun  41049  ovn0ssdmfun  41052  plusfreseq  41057  idfusubc0  41150  rhmsubclem2  41372  rhmsubcALTVlem2  41390  lmod1lem2  41562  lmod1lem3  41563  logb2aval  41805
  Copyright terms: Public domain W3C validator