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

Theorem oveq2i 6812
Description: Equality inference for operation value. (Contributed by NM, 28-Feb-1995.)
Hypothesis
Ref Expression
oveq1i.1 𝐴 = 𝐵
Assertion
Ref Expression
oveq2i (𝐶𝐹𝐴) = (𝐶𝐹𝐵)

Proof of Theorem oveq2i
StepHypRef Expression
1 oveq1i.1 . 2 𝐴 = 𝐵
2 oveq2 6809 . 2 (𝐴 = 𝐵 → (𝐶𝐹𝐴) = (𝐶𝐹𝐵))
31, 2ax-mp 5 1 (𝐶𝐹𝐴) = (𝐶𝐹𝐵)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1620  (class class class)co 6801
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1859  ax-4 1874  ax-5 1976  ax-6 2042  ax-7 2078  ax-9 2136  ax-10 2156  ax-11 2171  ax-12 2184  ax-13 2379  ax-ext 2728
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1623  df-ex 1842  df-nf 1847  df-sb 2035  df-clab 2735  df-cleq 2741  df-clel 2744  df-nfc 2879  df-rex 3044  df-rab 3047  df-v 3330  df-dif 3706  df-un 3708  df-in 3710  df-ss 3717  df-nul 4047  df-if 4219  df-sn 4310  df-pr 4312  df-op 4316  df-uni 4577  df-br 4793  df-iota 6000  df-fv 6045  df-ov 6804
This theorem is referenced by:  caov32  7014  caov4  7018  caov42  7020  seqomsuc  7709  oa1suc  7768  o2p2e4  7778  om1  7779  oe1  7781  oawordeulem  7791  oeoalem  7833  nnm1  7885  nnm2  7886  nneob  7889  omopthlem1  7892  mapsnconst  8057  mapsncnv  8058  map2xp  8283  cantnflt  8730  cnfcom2  8760  infxpenc  9002  infxpenc2  9006  ackbij1lem5  9209  alephom  9570  pwxpndom2  9650  adderpqlem  9939  addassnq  9943  mulcanenq  9945  distrnq  9946  ltanq  9956  ltexnq  9960  halfnq  9961  ltrnq  9964  archnq  9965  addclprlem2  10002  prlem934  10018  prlem936  10032  addcmpblnr  10053  mulcmpblnrlem  10054  ltsrpr  10061  m1p1sr  10076  m1m1sr  10077  0idsr  10081  1idsr  10082  00sr  10083  pn0sr  10085  recexsrlem  10087  mulgt0sr  10089  sqgt0sr  10090  mulresr  10123  axmulcom  10139  axmulass  10141  axdistr  10142  axi2m1  10143  ax1rid  10145  axcnre  10148  mul02lem1  10375  addid1  10379  negid  10491  negsub  10492  subneg  10493  negsubdii  10529  muleqadd  10834  crne0  11176  2p2e4  11307  3p2e5  11323  3p3e6  11324  4p2e6  11325  4p3e7  11326  4p4e8  11327  5p2e7  11328  5p3e8  11329  5p4e9  11330  5p5e10OLD  11331  6p2e8  11332  6p3e9  11333  6p4e10OLD  11334  7p2e9  11335  7p3e10OLD  11336  8p2e10OLD  11337  3t3e9  11343  8th4div3  11415  halfpm6th  11416  addltmul  11431  div4p1lem1div2  11450  nn0n0n1ge2  11521  nneo  11624  zeo  11626  numsuc  11674  numltc  11691  numsucc  11712  numma  11720  nummul1c  11725  decrmac  11740  decsubi  11746  decsubiOLD  11747  decmul1  11748  decmul10add  11756  decmul10addOLD  11757  6p5lem  11758  5p5e10  11759  6p4e10  11761  7p3e10  11766  8p2e10  11773  4t3lem  11794  9t11e99  11834  9t11e99OLD  11835  decbin2  11846  xmulmnf1  12270  fztp  12561  fzprval  12565  fztpval  12566  fzshftral  12592  fz0tp  12605  fz0to3un2pr  12606  fzo01  12715  fzo12sn  12716  fzo13pr  12717  fzo0to2pr  12718  fzo0to3tp  12719  fzo0to42pr  12720  fzo1to4tp  12721  fzosplitprm1  12743  quoremz  12819  quoremnn0ALT  12821  intfrac2  12822  intfracq  12823  sqval  13087  sqrecii  13111  sq4e2t8  13127  cu2  13128  i3  13131  i4  13132  binom2i  13139  binom3  13150  crreczi  13154  3dec  13215  sq10OLD  13216  3decOLD  13218  nn0opthlem1  13220  facp1  13230  faclbnd  13242  faclbnd2  13243  faclbnd4lem1  13245  faclbnd4lem4  13248  bcn1  13265  bcn2  13271  4bc3eq4  13280  4bc2eq6  13281  hashgadd  13329  hashxplem  13383  hashmap  13385  hashfun  13387  hashbclem  13399  fz1isolem  13408  ccatlid  13529  ccatrid  13530  ccats1val2  13572  ccat2s1p2  13575  wrdeqs1cat  13645  swrdccatin12lem3  13661  swrdccat3a  13665  cats1fvn  13774  cats1cat  13777  cats2cat  13778  s3fn  13827  swrds2  13856  swrds2m  13857  reim0  14028  cji  14069  sqrtm1  14186  absi  14196  rddif  14250  iseraltlem2  14583  iseralt  14585  fsump1i  14670  fsummulc2  14686  incexclem  14738  incexc  14739  arisum2  14763  geoihalfsum  14784  mertenslem1  14786  mertens  14788  risefall0lem  14927  risefac1  14934  fallfac1  14935  fallfacfwd  14937  bpoly0  14951  bpoly1  14952  bpolydiflem  14955  bpoly2  14958  bpoly3  14959  bpoly4  14960  fsumcube  14961  ef0lem  14979  ege2le3  14990  eft0val  15012  ef4p  15013  efgt1p2  15014  efgt1p  15015  tanval2  15033  efival  15052  ef01bndlem  15084  sin01bnd  15085  cos01bnd  15086  cos1bnd  15087  cos2bnd  15088  rpnnen2lem11  15123  sqrt2irrlemOLD  15148  3dvdsdec  15227  3dvdsdecOLD  15228  3dvds2dec  15229  3dvds2decOLD  15230  odd2np1lem  15237  odd2np1  15238  oddp1even  15241  opoe  15260  divalglem5  15293  divalglem6  15294  bits0  15323  0bits  15334  gcdaddmlem  15418  6gcd4e2  15428  lcmneg  15489  3lcm2e6woprm  15501  6lcm4e12  15502  3prm  15579  3lcm2e6  15613  phiprm  15655  eulerthlem2  15660  prmdiv  15663  pythagtriplem12  15704  pythagtriplem14  15706  pcmpt  15769  pcfac  15776  prmpwdvds  15781  pockthi  15784  prmreclem2  15794  prmreclem6  15798  4sqlem5  15819  4sqlem13  15834  modxai  15945  mod2xnegi  15948  gcdi  15950  decexp2  15952  numexpp1  15955  numexp2x  15956  decsplit0b  15957  decsplit1  15959  decsplit  15960  decsplit0bOLD  15961  decsplit1OLD  15963  decsplitOLD  15964  2exp16  15970  prmlem0  15985  139prm  16004  163prm  16005  317prm  16006  631prm  16007  1259lem4  16014  1259lem5  16015  1259prm  16016  2503lem1  16017  2503lem2  16018  2503lem3  16019  2503prm  16020  4001lem1  16021  4001lem4  16024  ressinbas  16109  rcaninv  16626  rescfth  16769  xpccatid  17000  oduval  17302  oppgmnd  17955  psgnunilem2  18086  psgnunilem4  18088  psgnpmtr  18101  psgn0fv0  18102  psgnsn  18111  psgnprfval1  18113  lsmmod2  18260  efgi0  18304  efgi1  18305  efginvrel2  18311  efgsval2  18317  efgsp1  18321  efgredleme  18327  efgredlemc  18329  efgcpbllemb  18339  frgpnabllem1  18447  lt6abl  18467  gsumconstf  18506  gsum2dlem2  18541  pwsgsum  18549  fsfnn0gsumfsffz  18550  dprd0  18601  dprdf1  18603  dprd2da  18612  ablfac1lem  18638  pgpfac1lem3  18647  pgpfaclem1  18651  srgbinomlem4  18714  opprring  18802  mulgass3  18808  evlsval  19692  mpff  19706  ply1assa  19742  gsumply1subr  19777  ply1coe  19839  coe1fzgsumdlem  19844  coe1fzgsumd  19845  gsumply1eq  19848  evl1gsumdlem  19893  evl1gsumd  19894  xrsnsgrp  19955  znbas  20065  znzrh2  20067  dsmmval2  20253  frlmip  20290  matgsum  20416  madetsumid  20440  mdetrsca  20582  mdetrsca2  20583  mdettpos  20590  m2detleiblem2  20607  madugsum  20622  madurid  20623  cpmat  20687  pmatcollpwfi  20760  pmatcollpw3fi1lem1  20764  pm2mpval  20773  mp2pm2mplem5  20788  chpmat1dlem  20813  chpmat1d  20814  chpidmat  20825  cpmidpmat  20851  cpmadugsumfi  20855  chcoeffeqlem  20863  cayleyhamilton0  20867  cayleyhamiltonALT  20869  cayleyhamilton1  20870  restin  21143  imacmp  21373  conncompconn  21408  uptx  21601  cnpflf2  21976  tmdgsum2  22072  tsmsres  22119  tsmsf1o  22120  tsmsmhm  22121  prdsxmet  22346  resspwsds  22349  prdsxmslem2  22506  tngngpim  22635  metdcn2  22814  metdcn  22815  metdscn2  22832  iimulcn  22909  icchmeo  22912  xrhmeo  22917  cnrehmeo  22924  cnheiborlem  22925  evth  22930  evth2  22931  lebnumlem2  22933  reparphti  22968  pcoass  22995  pi1xfrcnv  23028  ipcau2  23204  minveclem4  23374  pjthlem1  23379  ovolunlem1a  23435  unmbl  23476  uniioombl  23528  iblitg  23705  dfitg  23706  itg0  23716  iblcnlem1  23724  itgcnlem  23726  itgabs  23771  limcdif  23810  limccnp  23825  limccnp2  23826  dvexp  23886  dvmptid  23890  dvmptc  23891  dvmptfsum  23908  dveflem  23912  dvsincos  23914  mvth  23925  dvlipcn  23927  dvivthlem1  23941  dvfsumle  23954  dvfsumlem2  23960  itgsubst  23982  tdeglem4  23990  tdeglem2  23991  plypf1  24138  plymullem1  24140  coesub  24183  dgrmulc  24197  fta1lem  24232  vieta1lem1  24235  vieta1lem2  24236  aalioulem4  24260  aaliou3lem3  24269  abelthlem2  24356  abelthlem8  24363  abelthlem9  24364  sinhalfpilem  24385  efhalfpi  24393  cospi  24394  efipi  24395  sin2pi  24397  cos2pi  24398  ef2pi  24399  sin2pim  24407  cos2pim  24408  sinmpi  24409  cosmpi  24410  sinppi  24411  cosppi  24412  sincosq4sgn  24423  tangtx  24427  sincos4thpi  24435  sincos6thpi  24437  sincos3rdpi  24438  pige3  24439  abssinper  24440  efif1olem4  24461  efifo  24463  eff1o  24465  circgrp  24468  circsubm  24469  logneg  24504  logimul  24530  logneg2  24531  dvrelog  24553  logcnlem4  24561  dvlog  24567  dvlog2  24569  logtayl  24576  1cxp  24588  ecxp  24589  cxpsqrt  24619  dvsqrt  24653  dvcnsqrt  24655  root1eq1  24666  cxpeq  24668  elogb  24678  ang180lem1  24709  ang180lem2  24710  heron  24735  1cubrlem  24738  1cubr  24739  dcubic2  24741  mcubic  24744  cubic2  24745  binom4  24747  dquartlem1  24748  dquartlem2  24749  dquart  24750  quart1lem  24752  quart1  24753  quartlem1  24754  asinsin  24789  asin1  24791  acos1  24792  atanlogsublem  24812  atanlogsub  24813  efiatan2  24814  2efiatan  24815  tanatan  24816  atanbnd  24823  atan1  24825  dvatan  24832  atantayl2  24835  leibpilem2  24838  leibpi  24839  log2cnv  24841  log2tlbnd  24842  log2ublem1  24843  log2ublem2  24844  log2ublem3  24845  log2ub  24846  birthday  24851  amgmlem  24886  emcllem5  24896  lgamgulmlem2  24926  lgamgulmlem5  24929  lgam1  24960  wilthlem2  24965  ftalem6  24974  basellem2  24978  basellem3  24979  basellem5  24981  basellem8  24984  cht1  25061  chp1  25063  1sgmprm  25094  ppiublem2  25098  ppiub  25099  chtublem  25106  chtub  25107  logfacbnd3  25118  bcp1ctr  25174  bclbnd  25175  bposlem1  25179  bposlem4  25182  bposlem6  25184  bposlem8  25186  bposlem9  25187  lgslem1  25192  lgsdir2lem1  25220  lgsdir2lem2  25221  lgsdir2lem3  25222  lgsdir2lem5  25224  lgs1  25236  gausslemma2dlem1a  25260  gausslemma2dlem3  25263  gausslemma2dlem4  25264  gausslemma2d  25269  lgseisenlem1  25270  lgseisenlem3  25272  lgsquadlem1  25275  lgsquadlem2  25276  lgsquad2lem2  25280  m1lgs  25283  2lgslem1a2  25285  2sqlem8  25321  2sqblem  25326  logdivsum  25392  mulog2sumlem2  25394  log2sumbnd  25403  selberglem1  25404  selberglem2  25405  pntrmax  25423  pntibndlem2  25450  pntibndlem3  25451  pntlemg  25457  pntlemr  25461  pntlemo  25466  ostth2lem3  25494  ostth2lem4  25495  istrkg3ld  25530  trgcgrg  25580  tgcgr4  25596  colperpexlem1  25792  ax5seglem7  25985  axlowdimlem4  25995  axlowdimlem16  26007  setsiedg  26098  vdegp1ci  26615  finsumvtxdg2sstep  26626  finsumvtxdg2size  26627  wlkp1lem6  26756  wlkp1lem8  26758  wlkp1  26759  uhgrwkspthlem2  26831  pthdlem1  26843  pthdlem2  26845  pthd  26846  crctcshwlkn0lem4  26887  crctcshwlkn0lem5  26888  crctcshwlkn0lem6  26889  crctcshlem4  26894  crctcshwlkn0  26895  2wlkdlem2  27017  2wlkdlem4  27019  2pthdlem1  27021  wwlks2onv  27044  clwlkclwwlk2  27097  wwlksext2clwwlk  27158  wwlksext2clwwlkOLD  27159  clwwlknonex2lem1  27227  0ewlk  27237  1ewlk  27238  0wlk  27239  1pthdlem1  27258  1pthdlem2  27259  1wlkdlem1  27260  1wlkdlem4  27263  wlk2v2e  27280  3wlkdlem2  27283  3wlkdlem4  27285  3pthdlem1  27287  eupth0  27337  eupthp1  27339  eucrctshift  27366  eucrct2eupth  27368  extwwlkfablem1OLD  27468  numclwlk1lem2foalem  27481  numclwlk2lem2f  27509  numclwlk2lem2fOLD  27516  frgrregord013  27534  ex-exp  27589  ex-bc  27591  ex-gcd  27596  ex-lcm  27597  ex-ind-dvds  27600  smcnlem  27832  ipidsq  27845  dipcj  27849  dip0r  27852  nmlnoubi  27931  nmblolbii  27934  blocnilem  27939  ip1ilem  27961  ip2i  27963  ipdirilem  27964  ipasslem10  27974  ipasslem11  27975  siilem1  27986  hvmul0  28161  hvsubsub4i  28196  hvnegdii  28199  hvsubeq0i  28200  hvsubcan2i  28201  hvsubaddi  28203  hvsub0  28213  hisubcomi  28241  normlem0  28246  normlem1  28247  normlem2  28248  normlem3  28249  normlem9  28255  norm-ii-i  28274  norm3difi  28284  normpari  28291  polid2i  28294  polidi  28295  bcsiALT  28316  pjhthlem1  28530  chdmm3i  28618  chdmm4i  28619  chjidm  28659  chj4i  28662  chjjdiri  28663  spanunsni  28718  pjoml4i  28726  cmcm2i  28732  qlax4i  28769  qlax5i  28770  pjadjii  28813  pjmulii  28816  pjsubii  28817  pjssmii  28820  pjcji  28823  pjneli  28862  hoadd32i  28917  ho0subi  28934  hosubid1  28937  hosd2i  28962  hopncani  28963  hosubeq0i  28965  lnopeq0lem1  29144  lnopunilem1  29149  lnophmlem2  29156  nmbdoplbi  29163  nmcopexi  29166  lnfnmuli  29183  nmcfnexi  29190  nmoptri2i  29238  nmopcoadji  29240  golem1  29410  mdsl1i  29460  cvmdi  29463  mdslmd3i  29471  csmdsymi  29473  dfdec100  29856  dfdp2OLD  29859  dp20u  29865  dpmul10  29883  dpmul100  29885  dp3mul10  29886  dpmul1000  29887  dpexpp1  29896  0dp2dp  29897  dpmul  29901  dpmul4  29902  1mhdrd  29904  xrge00  29966  archirngz  30023  archiabllem2c  30029  gsumle  30059  gsummpt2co  30060  gsumvsca1  30062  gsumvsca2  30063  xrge0slmod  30124  psgnfzto1st  30135  lmat22det  30168  madjusmdetlem4  30176  raddcn  30255  xrge0iifhom  30263  xrge0mulc1cn  30267  cbvesum  30384  gsumesum  30401  esumpfinvallem  30416  esumpfinvalf  30418  dya2icoseg  30619  sitg0  30688  eulerpartlemd  30708  eulerpartlemgvv  30718  eulerpartlemgh  30720  fib0  30741  fib1  30742  fibp1  30743  orrvcval4  30806  orrvcoel  30807  orrvccel  30808  coinflipprob  30821  coinflippvt  30826  ballotlem2  30830  ballotth  30879  signstf0  30925  signstfvn  30926  signsvtn0  30927  signstfvp  30928  signstfveq0  30934  signsvf0  30937  signsvf1  30938  signsvfn  30939  signshf  30945  prodfzo03  30961  itgexpif  30964  repr0  30969  hgt750lemd  31006  hgt750lem  31009  hgt750lem2  31010  subfacp1lem1  31439  subfacp1lem5  31444  subfacval2  31447  subfaclim  31448  subfacval3  31449  cvxpconn  31502  cvxsconn  31503  mrsub0  31691  problem4  31840  quad3  31842  sinccvglem  31844  iexpire  31899  faclimlem1  31907  frrlem5  32061  fwddifnp1  32549  knoppcnlem10  32769  knoppndvlem7  32786  knoppndvlem21  32800  cnndvlem1  32805  finxpreclem4  33513  ptrest  33690  poimirlem27  33718  dvtan  33742  itgabsnc  33761  ftc1anclem8  33774  dvasin  33778  dvacos  33779  areacirclem1  33782  areacirclem4  33785  areacirc  33787  prdstotbnd  33875  prdsbnd2  33876  repwsmet  33915  rrnequiv  33916  reheibor  33920  dalem-cly  35429  pmodN  35608  cdleme0cp  35973  cdleme0cq  35974  cdleme1  35986  cdleme3d  35990  cdleme3h  35994  cdleme4  35997  cdleme5  35999  cdleme7a  36002  cdleme8  36009  cdleme9  36012  cdleme10  36013  cdleme11g  36024  cdleme15b  36034  cdleme21  36096  cdleme22e  36103  cdleme22eALTN  36104  cdleme23c  36110  cdleme25cv  36117  cdleme35b  36209  cdleme35c  36210  cdleme42a  36230  cdleme42d  36232  cdleme43aN  36248  cdlemeg46gfv  36289  cdlemk35  36671  dihjatcclem1  37178  lcdval2  37350  mapdpglem21  37452  mapfzcons  37750  mapfzcons1cl  37752  2rexfrabdioph  37831  3rexfrabdioph  37832  4rexfrabdioph  37833  6rexfrabdioph  37834  7rexfrabdioph  37835  rabdiophlem2  37837  diophren  37848  rabren3dioph  37850  pellexlem5  37868  pell1qr1  37906  rmspecfund  37945  jm2.17a  37998  jm2.17b  37999  jm2.27c  38045  jm2.27dlem5  38051  lmhmlnmsplit  38128  arearect  38272  areaquad  38273  relexp2  38440  trclfvdecomr  38491  k0004val0  38923  inductionexd  38924  unitadd  38969  amgm2d  38972  amgm3d  38973  lhe4.4ex1a  38999  expgrowthi  39003  expgrowth  39005  bccn1  39014  binomcxplemdvbinom  39023  binomcxplemdvsum  39025  binomcxplemnotnn0  39026  binomcxp  39027  refsumcn  39657  unirnmapsn  39874  oddfl  39957  infleinflem2  40054  sumnnodd  40334  cosnegpi  40550  dvcosre  40598  dvsinax  40599  ioodvbdlimc1lem2  40619  ioodvbdlimc2lem  40621  dvmptmulf  40624  dvxpaek  40627  dvmptfprod  40632  dvnprodlem2  40634  dvnprodlem3  40635  itgsin0pilem1  40637  itgsinexplem1  40641  itgsubsticclem  40663  stoweidlem13  40702  wallispilem4  40757  wallispi2lem1  40760  wallispi2lem2  40761  stirlinglem1  40763  dirkerper  40785  dirkertrigeqlem1  40787  dirkertrigeqlem3  40789  dirkertrigeq  40790  dirkeritg  40791  dirkercncflem1  40792  dirkercncflem2  40793  fourierdlem36  40832  fourierdlem41  40837  fourierdlem42  40838  fourierdlem48  40843  fourierdlem56  40851  fourierdlem57  40852  fourierdlem58  40853  fourierdlem60  40855  fourierdlem61  40856  fourierdlem62  40857  fourierdlem65  40860  fourierdlem73  40868  fourierdlem80  40875  fourierdlem87  40882  fourierdlem89  40884  fourierdlem90  40885  fourierdlem91  40886  fourierdlem100  40895  fourierdlem103  40898  fourierdlem107  40902  fourierdlem112  40907  fourierdlem113  40908  fourierdlem115  40910  fouriercnp  40915  sqwvfoura  40917  sqwvfourb  40918  fourierswlem  40919  fouriersw  40920  etransclem2  40925  etransclem37  40960  etransclem46  40969  hoidmvlelem3  41286  vonioolem2  41370  issmflem  41411  smfmullem2  41474  1t10e1p1e11  41798  1t10e1p1e11OLD  41799  pfx1  41890  pfxccatpfx1  41906  pfxccatpfx2  41907  fmtno0  41931  fmtno1  41932  fmtnorec2lem  41933  fmtnorec3  41939  fmtno2  41941  fmtno3  41942  fmtno4  41943  fmtno4sqrt  41962  fmtno4prmfac  41963  2exp5  41986  139prmALT  41990  31prm  41991  2exp7  41993  2exp11  41996  mod42tp1mod8  41998  lighneallem2  42002  5tcu2e40  42011  3exp4mod41  42012  41prothprmlem1  42013  41prothprmlem2  42014  41prothprm  42015  bits0ALTV  42069  sbgoldbo  42154  nnsum3primes4  42155  nnsum3primesgbe  42159  nnsum4primesodd  42163  nnsum4primesoddALTV  42164  nnsum4primeseven  42167  nnsum4primesevenALTV  42168  bgoldbtbndlem1  42172  tgoldbachlt  42183  tgoldbachltOLD  42189  2t6m3t4e0  42605  zlmodzxzequa  42764  zlmodzxznm  42765  zlmodzxzequap  42767  nn0sumshdiglemA  42892  nn0sumshdiglemB  42893  nn0sumshdiglem1  42894  sec0  42983  amgmw2d  43032
  Copyright terms: Public domain W3C validator