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 6530
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 11007). This definition is well-defined, although not very meaningful, when classes 𝐴 and/or 𝐵 are proper classes (i.e. are not sets); see ovprc1 6560 and ovprc2 6561. On the other hand, we often find uses for this definition when 𝐹 is a proper class, such as +𝑜 in oav 7455. 𝐹 is normally equal to a class of nested ordered pairs of the form defined by df-oprab 6531. (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 6527 . 2 class (𝐴𝐹𝐵)
51, 2cop 4130 . . 3 class 𝐴, 𝐵
65, 3cfv 5790 . 2 class (𝐹‘⟨𝐴, 𝐵⟩)
74, 6wceq 1474 1 wff (𝐴𝐹𝐵) = (𝐹‘⟨𝐴, 𝐵⟩)
Colors of variables: wff setvar class
This definition is referenced by:  oveq  6533  oveq1  6534  oveq2  6535  nfovd  6552  ovex  6555  ovssunirn  6557  0ov  6558  ovprc  6559  csbov123  6563  csbov  6564  elovimad  6569  fnotovb  6570  ffnov  6640  eqfnov  6642  fnov  6644  ovid  6653  ovidig  6654  ov  6656  ovigg  6657  ov6g  6674  ovg  6675  ovres  6676  fovrn  6679  fnrnov  6682  foov  6683  fnovrn  6684  funimassov  6686  ovelimab  6687  ovima0  6688  ovconst2  6689  oprssdm  6690  nssdmovg  6691  ndmovg  6692  elmpt2cl  6751  1st2val  7062  2nd2val  7063  brovpreldm  7118  bropopvvv  7119  bropfvvvvlem  7120  ovmptss  7122  oprab2co  7126  curry1  7133  curry2  7136  algrflem  7150  mpt2xeldm  7201  mpt2xopn0yelv  7203  mpt2xopxnop0  7205  ovtpos  7231  mpt2curryd  7259  seqomlem1  7409  seqomlem4  7412  brwitnlem  7451  cantnfvalf  8422  fseqenlem1  8707  axdc4lem  9137  fpwwe  9324  canthwelem  9328  addpiord  9562  mulpiord  9563  addpqnq  9616  mulpqnq  9619  recmulnq  9642  dmrecnq  9646  cnref1o  11659  ixxssxr  12014  om2uzrdg  12572  uzrdgsuci  12576  swrd00  13216  swrd0  13232  cnrecnv  13699  sadcf  14959  smupf  14984  eucalgval  15079  eucalginv  15081  eucalglt  15082  eucalg  15084  vdwmc  15466  isstruct2  15650  isstruct  15651  imasaddvallem  15958  imasvscafn  15966  imasvscaval  15967  xpsff1o  15997  xpsaddlem  16004  xpsvsca  16008  xpsle  16010  comffval  16128  comfffval2  16130  comfeq  16135  isoval  16194  brcic  16227  isssc  16249  isfuncd  16294  funcf2  16297  idfu2nd  16306  idfucl  16310  cofucl  16317  resfval2  16322  resf2nd  16324  funcres2b  16326  funcpropd  16329  homaval  16450  homarcl2  16454  arwhoma  16464  coapm  16490  catcco  16520  catcisolem  16525  xpcco  16592  xpcid  16598  xpcpropd  16617  evlfcllem  16630  evlfcl  16631  curf1cl  16637  curf2cl  16640  curfcl  16641  uncf1  16645  uncf2  16646  uncfcurf  16648  diag11  16652  diag12  16653  diag2  16654  curf2ndf  16656  hof2fval  16664  hofcl  16668  hofpropd  16676  yonedalem21  16682  yonedalem22  16687  yonedalem3b  16688  yonedalem3  16689  yonedainv  16690  yonffthlem  16691  joinval  16774  meetval  16788  plusffval  17016  mgm1  17026  sgrp1  17062  mnd1  17100  mnd1id  17101  grp1  17291  gaid  17501  efgmnvl  17896  efgval2  17906  vrgpinv  17951  frgpuptinv  17953  frgpuplem  17954  frgpup2  17958  frgpup3lem  17959  frgpnabllem1  18045  gsum2dlem1  18138  gsum2dlem2  18139  gsum2d  18140  gsum2d2lem  18141  gsumcom2  18143  eldprd  18172  dprd2dlem2  18208  dprd2dlem1  18209  dprd2da  18210  srgfcl  18284  ring1  18371  scaffval  18650  ply1frcl  19450  ipffval  19757  mamudi  19970  mamudir  19971  mamuvs1  19972  mamuvs2  19973  matplusgcell  20000  matsubgcell  20001  matvscacell  20003  mat1dimmul  20043  mat1rhmelval  20047  mdetrlin  20169  mdetrsca  20170  pmatcoe1fsupp  20267  iccordt  20770  iscnp2  20795  ptbasfi  21136  txcnpi  21163  txdis1cn  21190  lmcn2  21204  xkococn  21215  cnmpt12f  21221  cnmpt21  21226  cnmpt2t  21228  cnmpt22  21229  cnmpt2k  21243  xkohmeo  21370  flfcnp2  21563  tmdcn2  21645  clssubg  21664  tgphaus  21672  qustgplem  21676  psmetxrge0  21870  imasdsf1olem  21929  xpsdsval  21937  xmeterval  21988  comet  22069  txmetcnp  22103  metustid  22110  metustsym  22111  metustexhalf  22112  blval2  22118  metuel2  22121  nrmmetd  22130  nmfval  22144  isngp3  22153  ngpds  22158  tngnm  22203  qtopbaslem  22304  cnmetdval  22316  remetdval  22332  tgqioo  22343  bndth  22496  htpyco2  22517  phtpyco2  22528  caubl  22831  caublcls  22832  bcthlem1  22846  bcthlem2  22847  bcthlem4  22849  bcthlem5  22850  ovolfioo  22960  ovolficc  22961  ovolficcss  22962  ovolfsval  22963  ovolctb  22982  ovoliunlem2  22995  ovolicc2lem1  23009  ovolicc2lem5  23013  ovolfs2  23062  ioorinv  23067  uniiccdif  23069  uniioovol  23070  uniiccvol  23071  uniioombllem2a  23073  uniioombllem2  23074  uniioombllem3a  23075  uniioombllem3  23076  uniioombllem4  23077  uniioombllem5  23078  uniioombllem6  23079  dyadovol  23084  dyadss  23085  dyaddisjlem  23086  dyadmaxlem  23088  dyadmbl  23091  opnmbllem  23092  itg1addlem4  23189  limccnp2  23379  dvbsss  23389  perfdvf  23390  dvdsmulf1o  24637  fsumdvdsmul  24638  fsumvma  24655  tglngne  25163  ltgseg  25209  tgelrnln  25243  edgov  25636  usgraexmplvtx  25697  usgraexmplcvtx  25700  usgraexmplcedg  25701  2wlkonot3v  26168  2spthonot3v  26169  isrgrac  26227  imsdval  26722  ofresid  28630  ofoprabco  28653  xrofsup  28729  smatrcl  28996  smatlem  28997  fvproj  29033  elunirnmbfm  29448  sibfof  29535  oddpwdcv  29550  eulerpartlemgh  29573  cndprobval  29628  cvmlift2lem9  30353  cvmlift2lem10  30354  cvmlift2lem13  30357  cvmliftphtlem  30359  fvtransport  31115  fvray  31224  linedegen  31226  fvline  31227  bj-finsumval0  32120  icoreunrn  32179  relowlpssretop  32184  finxpreclem1  32198  finxpreclem2  32199  finxpreclem3  32202  finxpreclem5  32204  curfv  32355  uncov  32356  curunc  32357  opnmbllem0  32411  mblfinlem1  32412  mblfinlem2  32413  ftc1anc  32459  ftc2nc  32460  opropabco  32484  f1opr  32485  ismtyhmeolem  32569  heiborlem3  32578  heiborlem4  32579  heiborlem6  32581  heiborlem8  32583  grposnOLD  32647  fvovco  38172  volioof  38677  fvvolioof  38679  fvvolicof  38681  fourierdlem42  38839  hoi2toco  39294  ovolval2lem  39330  ovolval3  39334  ovolval4lem1  39336  ovolval5lem2  39340  ovnovollem1  39343  ovnovollem2  39344  smfpimbor1lem1  39480  aovfundmoveq  39708  aovpcov0  39717  aovnuoveq  39718  aovvoveq  39719  aov0ov0  39720  aovovn0oveq  39721  aov0nbovbi  39722  aovov0bi  39723  pfx00  40045  pfx0  40046  opvtxov  40233  opiedgov  40236  edgaov  40350  ovn0dmfun  41549  ovn0ssdmfun  41552  plusfreseq  41557  idfusubc0  41650  rhmsubclem2  41874  rhmsubcALTVlem2  41893  lmod1lem2  42066  lmod1lem3  42067  logb2aval  42270
  Copyright terms: Public domain W3C validator