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 6428
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 10914). This definition is well-defined, although not very meaningful, when classes 𝐴 and/or 𝐵 are proper classes (i.e. are not sets); see ovprc1 6458 and ovprc2 6459. On the other hand, we often find uses for this definition when 𝐹 is a proper class, such as +𝑜 in oav 7353. 𝐹 is normally equal to a class of nested ordered pairs of the form defined by df-oprab 6429. (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 6425 . 2 class (𝐴𝐹𝐵)
51, 2cop 4034 . . 3 class 𝐴, 𝐵
65, 3cfv 5689 . 2 class (𝐹‘⟨𝐴, 𝐵⟩)
74, 6wceq 1474 1 wff (𝐴𝐹𝐵) = (𝐹‘⟨𝐴, 𝐵⟩)
Colors of variables: wff setvar class
This definition is referenced by:  oveq  6431  oveq1  6432  oveq2  6433  nfovd  6450  ovex  6453  ovssunirn  6455  0ov  6456  ovprc  6457  csbov123  6461  csbov  6462  elovimad  6467  fnotovb  6468  ffnov  6538  eqfnov  6540  fnov  6542  ovid  6551  ovidig  6552  ov  6554  ovigg  6555  ov6g  6572  ovg  6573  ovres  6574  fovrn  6577  fnrnov  6580  foov  6581  fnovrn  6582  funimassov  6584  ovelimab  6585  ovima0  6586  ovconst2  6587  oprssdm  6588  nssdmovg  6589  ndmovg  6590  elmpt2cl  6649  1st2val  6959  2nd2val  6960  brovpreldm  7015  bropopvvv  7016  bropfvvvvlem  7017  ovmptss  7019  oprab2co  7023  curry1  7030  curry2  7033  algrflem  7047  mpt2xeldm  7098  mpt2xopn0yelv  7100  mpt2xopxnop0  7102  ovtpos  7128  mpt2curryd  7156  seqomlem1  7307  seqomlem4  7310  brwitnlem  7349  cantnfvalf  8320  fseqenlem1  8605  axdc4lem  9035  fpwwe  9222  canthwelem  9226  addpiord  9460  mulpiord  9461  addpqnq  9514  mulpqnq  9517  recmulnq  9540  dmrecnq  9544  cnref1o  11568  ixxssxr  11926  om2uzrdg  12484  uzrdgsuci  12488  swrd00  13127  swrd0  13143  cnrecnv  13610  sadcf  14884  smupf  14909  eucalgval  15007  eucalginv  15009  eucalglt  15010  eucalg  15012  vdwmc  15402  isstruct2  15586  isstruct  15587  imasaddvallem  15902  imasvscafn  15910  imasvscaval  15911  xpsff1o  15941  xpsaddlem  15948  xpsvsca  15952  xpsle  15954  comffval  16072  comfffval2  16074  comfeq  16079  isoval  16138  brcic  16171  isssc  16193  isfuncd  16238  funcf2  16241  idfu2nd  16250  idfucl  16254  cofucl  16261  resfval2  16266  resf2nd  16268  funcres2b  16270  funcpropd  16273  homaval  16394  homarcl2  16398  arwhoma  16408  coapm  16434  catcco  16464  catcisolem  16469  xpcco  16536  xpcid  16542  xpcpropd  16561  evlfcllem  16574  evlfcl  16575  curf1cl  16581  curf2cl  16584  curfcl  16585  uncf1  16589  uncf2  16590  uncfcurf  16592  diag11  16596  diag12  16597  diag2  16598  curf2ndf  16600  hof2fval  16608  hofcl  16612  hofpropd  16620  yonedalem21  16626  yonedalem22  16631  yonedalem3b  16632  yonedalem3  16633  yonedainv  16634  yonffthlem  16635  joinval  16718  meetval  16732  plusffval  16960  mgm1  16970  sgrp1  17006  mnd1  17044  mnd1id  17045  grp1  17235  gaid  17445  efgmnvl  17856  efgval2  17866  vrgpinv  17911  frgpuptinv  17913  frgpuplem  17914  frgpup2  17918  frgpup3lem  17919  frgpnabllem1  18004  gsum2dlem1  18097  gsum2dlem2  18098  gsum2d  18099  gsum2d2lem  18100  gsumcom2  18102  eldprd  18131  dprd2dlem2  18167  dprd2dlem1  18168  dprd2da  18169  srgfcl  18243  ring1  18330  scaffval  18609  ply1frcl  19406  ipffval  19716  mamudi  19929  mamudir  19930  mamuvs1  19931  mamuvs2  19932  matplusgcell  19959  matsubgcell  19960  matvscacell  19962  mat1dimmul  20002  mat1rhmelval  20006  mdetrlin  20128  mdetrsca  20129  pmatcoe1fsupp  20226  iccordt  20729  iscnp2  20754  ptbasfi  21095  txcnpi  21122  txdis1cn  21149  lmcn2  21163  xkococn  21174  cnmpt12f  21180  cnmpt21  21185  cnmpt2t  21187  cnmpt22  21188  cnmpt2k  21202  xkohmeo  21329  flfcnp2  21522  tmdcn2  21604  clssubg  21623  tgphaus  21631  qustgplem  21635  psmetxrge0  21829  imasdsf1olem  21888  xpsdsval  21896  xmeterval  21947  comet  22028  txmetcnp  22062  metustid  22069  metustsym  22070  metustexhalf  22071  blval2  22077  metuel2  22080  nrmmetd  22089  nmfval  22103  isngp3  22112  ngpds  22117  tngnm  22159  qtopbaslem  22279  cnmetdval  22291  remetdval  22307  tgqioo  22318  bndth  22486  htpyco2  22510  phtpyco2  22521  caubl  22778  caublcls  22779  bcthlem1  22793  bcthlem2  22794  bcthlem4  22796  bcthlem5  22797  ovolfioo  22919  ovolficc  22920  ovolficcss  22921  ovolfsval  22922  ovolctb  22941  ovoliunlem2  22954  ovolicc2lem1  22968  ovolicc2lem5  22972  ovolfs2  23021  ioorinv  23026  uniiccdif  23028  uniioovol  23029  uniiccvol  23030  uniioombllem2a  23032  uniioombllem2  23033  uniioombllem3a  23034  uniioombllem3  23035  uniioombllem4  23036  uniioombllem5  23037  uniioombllem6  23038  dyadovol  23043  dyadss  23044  dyaddisjlem  23045  dyadmaxlem  23047  dyadmbl  23050  opnmbllem  23051  itg1addlem4  23148  limccnp2  23338  dvbsss  23348  perfdvf  23349  dvdsmulf1o  24610  fsumdvdsmul  24611  fsumvma  24628  tglngne  25136  ltgseg  25182  tgelrnln  25216  edgov  25609  usgraexmplvtx  25670  usgraexmplcvtx  25673  usgraexmplcedg  25674  2wlkonot3v  26141  2spthonot3v  26142  isrgrac  26200  imsdval  26695  ofresid  28613  ofoprabco  28636  xrofsup  28719  smatrcl  28987  smatlem  28988  fvproj  29024  elunirnmbfm  29439  sibfof  29537  oddpwdcv  29552  eulerpartlemgh  29575  cndprobval  29630  cvmlift2lem9  30393  cvmlift2lem10  30394  cvmlift2lem13  30397  cvmliftphtlem  30399  fvtransport  31145  fvray  31254  linedegen  31256  fvline  31257  bj-finsumval0  32156  icoreunrn  32215  relowlpssretop  32220  finxpreclem1  32234  finxpreclem2  32235  finxpreclem3  32238  finxpreclem5  32240  curfv  32434  uncov  32435  curunc  32436  opnmbllem0  32490  mblfinlem1  32491  mblfinlem2  32492  ftc1anc  32538  ftc2nc  32539  opropabco  32563  f1opr  32564  ismtyhmeolem  32648  heiborlem3  32657  heiborlem4  32658  heiborlem6  32660  heiborlem8  32662  grposnOLD  32726  fvovco  38260  volioof  38770  fvvolioof  38772  fvvolicof  38774  fourierdlem42  38933  fourierdlem42OLD  38934  hoi2toco  39391  ovolval2lem  39427  ovolval3  39431  ovolval4lem1  39433  ovolval5lem2  39437  ovnovollem1  39440  ovnovollem2  39441  smfpimbor1lem1  39577  aovfundmoveq  39805  aovpcov0  39814  aovnuoveq  39815  aovvoveq  39816  aov0ov0  39817  aovovn0oveq  39818  aov0nbovbi  39819  aovov0bi  39820  pfx00  40142  pfx0  40143  opvtxov  40330  opiedgov  40333  edgaov  40447  ovn0dmfun  41646  ovn0ssdmfun  41649  plusfreseq  41654  idfusubc0  41747  rhmsubclem2  41971  rhmsubcALTVlem2  41990  lmod1lem2  42163  lmod1lem3  42164  logb2aval  42367
  Copyright terms: Public domain W3C validator