Theorem oveq2i 6921

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

Step	Hyp	Ref	Expression
1		oveq1i.1	. 2 ⊢ 𝐴 = 𝐵
2		oveq2 6918	. 2 ⊢ (𝐴 = 𝐵 → (𝐶𝐹𝐴) = (𝐶𝐹𝐵))
3	1, 2	ax-mp 5	1 ⊢ (𝐶𝐹𝐴) = (𝐶𝐹𝐵)

Syntax hints:   = wceq 1656  (class class class)co 6910

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1894  ax-4 1908  ax-5 2009  ax-6 2075  ax-7 2112  ax-9 2173  ax-10 2192  ax-11 2207  ax-12 2220  ax-13 2389  ax-ext 2803

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 879  df-3an 1113  df-tru 1660  df-ex 1879  df-nf 1883  df-sb 2068  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-rex 3123  df-rab 3126  df-v 3416  df-dif 3801  df-un 3803  df-in 3805  df-ss 3812  df-nul 4147  df-if 4309  df-sn 4400  df-pr 4402  df-op 4406  df-uni 4661  df-br 4876  df-iota 6090  df-fv 6135  df-ov 6913

This theorem is referenced by:  caov32  7126  caov4  7130  caov42  7132  seqomsuc  7823  oa1suc  7883  o2p2e4  7893  om1  7894  oe1  7896  oawordeulem  7906  oeoalem  7948  nnm1  8000  nnm2  8001  nneob  8004  omopthlem1  8007  mapsnconst  8176  mapsncnv  8177  map2xp  8405  cantnflt  8853  cnfcom2  8883  infxpenc  9161  infxpenc2  9165  ackbij1lem5  9368  alephom  9729  pwxpndom2  9809  adderpqlem  10098  addassnq  10102  mulcanenq  10104  distrnq  10105  ltanq  10115  ltexnq  10119  halfnq  10120  ltrnq  10123  archnq  10124  addclprlem2  10161  prlem934  10177  prlem936  10191  addcmpblnr  10213  mulcmpblnrlem  10214  ltsrpr  10221  m1p1sr  10236  m1m1sr  10237  0idsr  10241  1idsr  10242  00sr  10243  pn0sr  10245  recexsrlem  10247  mulgt0sr  10249  sqgt0sr  10250  mulresr  10283  axmulcom  10299  axmulass  10301  axdistr  10302  axi2m1  10303  ax1rid  10305  axcnre  10308  mul02lem1  10538  addid1  10542  negid  10656  negsub  10657  subneg  10658  negsubdii  10694  muleqadd  11003  crne0  11350  2p2e4  11500  1p2e3  11508  3p2e5  11516  3p3e6  11517  4p2e6  11518  4p3e7  11519  4p4e8  11520  5p2e7  11521  5p3e8  11522  5p4e9  11523  6p2e8  11524  6p3e9  11525  7p2e9  11526  3t3e9  11532  8th4div3  11585  halfpm6th  11586  addltmul  11601  div4p1lem1div2  11620  nn0n0n1ge2  11692  nneo  11796  zeo  11798  numsuc  11842  numltc  11855  numsucc  11869  numma  11873  nummul1c  11878  decrmac  11887  decsubi  11892  decmul1OLD  11894  decmul10add  11899  6p5lem  11900  5p5e10  11901  6p4e10  11902  7p3e10  11905  8p2e10  11910  4t3lem  11927  9t11e99  11960  decbin2  11971  xmulmnf1  12401  fztp  12697  fz12pr  12698  fzprval  12702  fztpval  12703  fzshftral  12729  fz0tp  12742  fz0to3un2pr  12743  fzo01  12852  fzo12sn  12853  fzo13pr  12854  fzo0to2pr  12855  fzo0to3tp  12856  fzo0to42pr  12857  fzo1to4tp  12858  fzosplitprm1  12880  quoremz  12956  quoremnn0ALT  12958  intfrac2  12959  intfracq  12960  sqval  13223  sqrecii  13247  sq4e2t8  13263  cu2  13264  i3  13267  i4  13268  binom2i  13275  binom3  13286  crreczi  13290  3dec  13353  nn0opthlem1  13355  facp1  13365  faclbnd  13377  faclbnd2  13378  faclbnd4lem1  13380  faclbnd4lem4  13383  bcn1  13400  bcn2  13406  4bc3eq4  13415  4bc2eq6  13416  hashgadd  13463  hashxplem  13516  hashmap  13518  hashfun  13520  hashbclem  13532  fz1isolem  13541  ccatlid  13653  ccatrid  13654  ccats1val2  13694  ccat2s1p2  13697  pfx1  13789  wrdeqs1catOLD  13817  swrdccatin12lem3  13837  pfxccatpfx1  13844  pfxccatpfx2  13845  swrdccat3aOLD  13847  cats1fvn  13986  cats1cat  13989  cats2cat  13990  s3fn  14039  swrds2  14068  swrds2m  14069  reim0  14242  cji  14283  sqrtm1  14400  absi  14410  rddif  14464  iseraltlem2  14797  iseralt  14799  fsump1i  14882  fsummulc2  14897  incexclem  14949  incexc  14950  arisum2  14974  geoihalfsum  14994  mertenslem1  14996  mertens  14998  risefall0lem  15136  risefac1  15143  fallfac1  15144  fallfacfwd  15146  bpoly0  15160  bpoly1  15161  bpolydiflem  15164  bpoly2  15167  bpoly3  15168  bpoly4  15169  fsumcube  15170  ef0lem  15188  ege2le3  15199  eft0val  15221  ef4p  15222  efgt1p2  15223  efgt1p  15224  tanval2  15242  efival  15261  ef01bndlem  15293  sin01bnd  15294  cos01bnd  15295  cos1bnd  15296  cos2bnd  15297  rpnnen2lem11  15334  3dvdsdec  15437  3dvds2dec  15438  odd2np1lem  15445  odd2np1  15446  oddp1even  15449  opoe  15468  divalglem5  15501  divalglem6  15502  bits0  15530  0bits  15541  gcdaddmlem  15625  6gcd4e2  15635  lcmneg  15696  3lcm2e6woprm  15708  6lcm4e12  15709  3prm  15785  3lcm2e6  15818  phiprm  15860  eulerthlem2  15865  prmdiv  15868  pythagtriplem12  15909  pythagtriplem14  15911  pcmpt  15974  pcfac  15981  prmpwdvds  15986  pockthi  15989  prmreclem2  15999  prmreclem6  16003  4sqlem5  16024  4sqlem13  16039  modxai  16150  mod2xnegi  16153  gcdi  16155  decexp2  16157  numexpp1  16160  numexp2x  16161  decsplit0b  16162  decsplit1  16164  decsplit  16165  2exp16  16170  prmlem0  16185  139prm  16203  163prm  16204  317prm  16205  631prm  16206  1259lem4  16213  1259lem5  16214  1259prm  16215  2503lem1  16216  2503lem2  16217  2503lem3  16218  2503prm  16219  4001lem1  16220  4001lem4  16223  ressinbas  16306  rcaninv  16813  rescfth  16956  xpccatid  17188  oduval  17490  oppgmnd  18141  psgnunilem2  18273  psgnunilem4  18275  psgnpmtr  18288  psgn0fv0  18289  psgnsn  18298  psgnprfval1  18300  lsmmod2  18447  efgi0  18491  efgi1  18492  efginvrel2  18498  efgsval2  18504  efgsp1  18508  efgredleme  18515  efgredlemc  18517  efgcpbllemb  18528  frgpnabllem1  18636  lt6abl  18656  gsumconstf  18695  gsum2dlem2  18730  pwsgsum  18738  fsfnn0gsumfsffz  18739  dprd0  18791  dprdf1  18793  dprd2da  18802  ablfac1lem  18828  pgpfac1lem3  18837  pgpfaclem1  18841  srgbinomlem4  18904  opprring  18992  mulgass3  18998  evlsval  19886  mpff  19900  ply1assa  19936  gsumply1subr  19971  ply1coe  20033  coe1fzgsumdlem  20038  coe1fzgsumd  20039  gsumply1eq  20042  evl1gsumdlem  20087  evl1gsumd  20088  xrsnsgrp  20149  znbas  20258  znzrh2  20260  dsmmval2  20450  frlmip  20491  matgsum  20617  madetsumid  20642  mdetrsca  20784  mdetrsca2  20785  mdettpos  20792  m2detleiblem2  20809  madugsum  20824  madurid  20825  cpmat  20891  pmatcollpwfi  20964  pmatcollpw3fi1lem1  20968  pm2mpval  20977  mp2pm2mplem5  20992  chpmat1dlem  21017  chpmat1d  21018  chpidmat  21029  cpmidpmat  21055  cpmadugsumfi  21059  chcoeffeqlem  21067  cayleyhamilton0  21071  cayleyhamiltonALT  21073  cayleyhamilton1  21074  restin  21348  imacmp  21578  conncompconn  21613  uptx  21806  cnpflf2  22181  tmdgsum2  22277  tsmsres  22324  tsmsf1o  22325  tsmsmhm  22326  prdsxmet  22551  resspwsds  22554  prdsxmslem2  22711  tngngpim  22840  metdcn2  23019  metdcn  23020  metdscn2  23037  iimulcn  23114  icchmeo  23117  xrhmeo  23122  cnrehmeo  23129  cnheiborlem  23130  evth  23135  evth2  23136  lebnumlem2  23138  reparphti  23173  pcoass  23200  pi1xfrcnv  23233  ipcau2  23409  ehl0base  23591  minveclem4  23607  pjthlem1  23612  ovolunlem1a  23669  unmbl  23710  uniioombl  23762  iblitg  23941  dfitg  23942  itg0  23952  iblcnlem1  23960  itgcnlem  23962  itgabs  24007  limcdif  24046  limccnp  24061  limccnp2  24062  dvexp  24122  dvmptid  24126  dvmptc  24127  dvmptfsum  24144  dveflem  24148  dvsincos  24150  mvth  24161  dvlipcn  24163  dvivthlem1  24177  dvfsumle  24190  dvfsumlem2  24196  itgsubst  24218  tdeglem4  24226  tdeglem2  24227  plypf1  24374  plymullem1  24376  coesub  24419  dgrmulc  24433  fta1lem  24468  vieta1lem1  24471  vieta1lem2  24472  aalioulem4  24496  aaliou3lem3  24505  abelthlem2  24592  abelthlem8  24599  abelthlem9  24600  sinhalfpilem  24622  efhalfpi  24630  cospi  24631  efipi  24632  sin2pi  24634  cos2pi  24635  ef2pi  24636  sin2pim  24644  cos2pim  24645  sinmpi  24646  cosmpi  24647  sinppi  24648  cosppi  24649  sincosq4sgn  24660  tangtx  24664  sincos4thpi  24672  sincos6thpi  24674  sincos3rdpi  24675  pige3  24676  abssinper  24677  efif1olem4  24698  efifo  24700  eff1o  24702  circgrp  24705  circsubm  24706  logneg  24740  logimul  24766  logneg2  24767  dvrelog  24789  logcnlem4  24797  dvlog  24803  dvlog2  24805  logtayl  24812  1cxp  24824  ecxp  24825  cxpsqrt  24855  2irrexpq  24882  dvsqrt  24892  dvcnsqrt  24894  root1eq1  24905  cxpeq  24907  elogb  24917  2logb9irrALT  24945  ang180lem1  24956  ang180lem2  24957  heron  24985  1cubrlem  24988  1cubr  24989  dcubic2  24991  mcubic  24994  cubic2  24995  binom4  24997  dquartlem1  24998  dquartlem2  24999  dquart  25000  quart1lem  25002  quart1  25003  quartlem1  25004  asinsin  25039  asin1  25041  acos1  25042  atanlogsublem  25062  atanlogsub  25063  efiatan2  25064  2efiatan  25065  tanatan  25066  atanbnd  25073  atan1  25075  dvatan  25082  atantayl2  25085  leibpilem2  25088  leibpi  25089  log2cnv  25091  log2tlbnd  25092  log2ublem1  25093  log2ublem2  25094  log2ublem3  25095  log2ub  25096  birthday  25101  amgmlem  25136  emcllem5  25146  lgamgulmlem2  25176  lgamgulmlem5  25179  lgam1  25210  wilthlem2  25215  ftalem6  25224  basellem2  25228  basellem3  25229  basellem5  25231  basellem8  25234  cht1  25311  chp1  25313  1sgmprm  25344  ppiublem2  25348  ppiub  25349  chtublem  25356  chtub  25357  logfacbnd3  25368  bcp1ctr  25424  bclbnd  25425  bposlem1  25429  bposlem4  25432  bposlem6  25434  bposlem8  25436  bposlem9  25437  lgslem1  25442  lgsdir2lem1  25470  lgsdir2lem2  25471  lgsdir2lem3  25472  lgsdir2lem5  25474  lgs1  25486  gausslemma2dlem1a  25510  gausslemma2dlem3  25513  gausslemma2dlem4  25514  gausslemma2d  25519  lgseisenlem1  25520  lgseisenlem3  25522  lgsquadlem1  25525  lgsquadlem2  25526  lgsquad2lem2  25530  m1lgs  25533  2lgslem1a2  25535  2sqlem8  25571  2sqblem  25576  logdivsum  25642  mulog2sumlem2  25644  log2sumbnd  25653  selberglem1  25654  selberglem2  25655  pntrmax  25673  pntibndlem2  25700  pntibndlem3  25701  pntlemg  25707  pntlemr  25711  pntlemo  25716  ostth2lem3  25744  ostth2lem4  25745  istrkg3ld  25780  trgcgrg  25834  tgcgr4  25850  colperpexlem1  26046  ax5seglem7  26241  axlowdimlem4  26251  axlowdimlem16  26263  setsiedg  26341  vdegp1ci  26843  finsumvtxdg2sstep  26854  finsumvtxdg2size  26855  wlkp1lem6  26986  wlkp1lem8  26988  wlkp1  26989  uhgrwkspthlem2  27063  pthdlem1  27075  pthdlem2  27077  pthd  27078  crctcshwlkn0lem4  27119  crctcshwlkn0lem5  27120  crctcshwlkn0lem6  27121  crctcshlem4  27126  crctcshwlkn0  27127  2wlkdlem2  27262  2wlkdlem4  27264  2pthdlem1  27266  wwlks2onv  27289  clwlkclwwlk2  27340  clwlkclwwlk2OLD  27341  wwlksext2clwwlk  27409  clwwlknonex2lem1  27478  0ewlk  27486  1ewlk  27487  0wlk  27488  1pthdlem1  27507  1pthdlem2  27508  1wlkdlem1  27509  1wlkdlem4  27512  wlk2v2e  27529  3wlkdlem2  27532  3wlkdlem4  27534  3pthdlem1  27536  eupth0  27586  eupthp1  27589  eucrctshift  27616  eucrct2eupthOLD  27619  eucrct2eupth  27620  numclwwlk1lem2foalem  27734  numclwwlk1lem2foalemOLD  27735  numclwlk2lem2f  27776  numclwlk2lem2fOLD  27779  numclwlk2lem2fOLDOLD  27787  frgrregord013  27806  ex-exp  27861  ex-bc  27863  ex-gcd  27868  ex-lcm  27869  ex-ind-dvds  27872  smcnlem  28103  ipidsq  28116  dipcj  28120  dip0r  28123  nmlnoubi  28202  nmblolbii  28205  blocnilem  28210  ip1ilem  28232  ip2i  28234  ipdirilem  28235  ipasslem10  28245  ipasslem11  28246  siilem1  28257  hvmul0  28432  hvsubsub4i  28467  hvnegdii  28470  hvsubeq0i  28471  hvsubcan2i  28472  hvsubaddi  28474  hvsub0  28484  hisubcomi  28512  normlem0  28517  normlem1  28518  normlem2  28519  normlem3  28520  normlem9  28526  norm-ii-i  28545  norm3difi  28555  normpari  28562  polid2i  28565  polidi  28566  bcsiALT  28587  pjhthlem1  28801  chdmm3i  28889  chdmm4i  28890  chjidm  28930  chj4i  28933  chjjdiri  28934  spanunsni  28989  pjoml4i  28997  cmcm2i  29003  qlax4i  29040  qlax5i  29041  pjadjii  29084  pjmulii  29087  pjsubii  29088  pjssmii  29091  pjcji  29094  pjneli  29133  hoadd32i  29188  ho0subi  29205  hosubid1  29208  hosd2i  29233  hopncani  29234  hosubeq0i  29236  lnopeq0lem1  29415  lnopunilem1  29420  lnophmlem2  29427  nmbdoplbi  29434  nmcopexi  29437  lnfnmuli  29454  nmcfnexi  29461  nmoptri2i  29509  nmopcoadji  29511  golem1  29681  mdsl1i  29731  cvmdi  29734  mdslmd3i  29742  csmdsymi  29744  dfdec100  30119  dp20u  30127  dpmul10  30144  dpmul100  30146  dp3mul10  30147  dpmul1000  30148  dpexpp1  30157  0dp2dp  30158  dpmul  30162  dpmul4  30163  1mhdrd  30165  xrge00  30227  archirngz  30284  archiabllem2c  30290  gsumle  30320  gsummpt2co  30321  gsumvsca1  30323  gsumvsca2  30324  xrge0slmod  30385  psgnfzto1st  30396  lmat22det  30429  madjusmdetlem4  30437  raddcn  30516  xrge0iifhom  30524  xrge0mulc1cn  30528  cbvesum  30645  gsumesum  30662  esumpfinvallem  30677  esumpfinvalf  30679  dya2icoseg  30880  sitg0  30949  eulerpartlemd  30969  eulerpartlemgvv  30979  eulerpartlemgh  30981  fib0  31003  fib1  31004  fibp1  31005  orrvcval4  31068  orrvcoel  31069  orrvccel  31070  coinflipprob  31083  coinflippvt  31088  ballotlem2  31092  ballotth  31141  signstf0  31188  signstfvn  31189  signsvtn0  31190  signsvtn0OLD  31191  signstfvp  31192  signstfveq0  31198  signstfveq0OLD  31199  signsvf0  31202  signsvf1  31203  signsvfn  31204  signshf  31210  prodfzo03  31226  itgexpif  31229  repr0  31234  hgt750lemd  31271  hgt750lem  31274  hgt750lem2  31275  subfacp1lem1  31703  subfacp1lem5  31708  subfacval2  31711  subfaclim  31712  subfacval3  31713  cvxpconn  31766  cvxsconn  31767  mrsub0  31955  problem4  32102  quad3  32104  sinccvglem  32106  iexpire  32159  faclimlem1  32167  frrlem5  32318  fwddifnp1  32806  knoppcnlem10  33020  knoppndvlem7  33036  knoppndvlem21  33050  cnndvlem1  33055  finxpreclem4  33775  ptrest  33951  poimirlem27  33979  dvtan  34002  itgabsnc  34021  ftc1anclem8  34034  dvasin  34038  dvacos  34039  areacirclem1  34042  areacirclem4  34045  areacirc  34047  prdstotbnd  34134  prdsbnd2  34135  repwsmet  34174  rrnequiv  34175  reheibor  34179  dalem-cly  35745  pmodN  35924  cdleme0cp  36288  cdleme0cq  36289  cdleme1  36301  cdleme3d  36305  cdleme3h  36309  cdleme4  36312  cdleme5  36314  cdleme7a  36317  cdleme8  36324  cdleme9  36327  cdleme10  36328  cdleme11g  36339  cdleme15b  36349  cdleme21  36411  cdleme22e  36418  cdleme22eALTN  36419  cdleme23c  36425  cdleme25cv  36432  cdleme35b  36524  cdleme35c  36525  cdleme42a  36545  cdleme42d  36547  cdleme43aN  36563  cdlemeg46gfv  36604  cdlemk35  36986  dihjatcclem1  37492  lcdval2  37664  mapdpglem21  37766  sqsumi  38055  sqmid3api  38057  sqn5ii  38060  sq3deccom12  38064  ex-decpmul  38066  mapfzcons  38122  mapfzcons1cl  38124  2rexfrabdioph  38203  3rexfrabdioph  38204  4rexfrabdioph  38205  6rexfrabdioph  38206  7rexfrabdioph  38207  rabdiophlem2  38209  diophren  38220  rabren3dioph  38222  pellexlem5  38240  pell1qr1  38278  rmspecfund  38316  jm2.17a  38369  jm2.17b  38370  jm2.27c  38416  jm2.27dlem5  38422  lmhmlnmsplit  38499  arearect  38642  areaquad  38643  relexp2  38809  trclfvdecomr  38860  k0004val0  39291  inductionexd  39292  unitadd  39337  amgm2d  39340  amgm3d  39341  lhe4.4ex1a  39367  expgrowthi  39371  expgrowth  39373  bccn1  39382  binomcxplemdvbinom  39391  binomcxplemdvsum  39393  binomcxplemnotnn0  39394  binomcxp  39395  refsumcn  40006  unirnmapsn  40211  oddfl  40286  infleinflem2  40382  sumnnodd  40655  cosnegpi  40871  dvcosre  40919  dvsinax  40920  ioodvbdlimc1lem2  40940  ioodvbdlimc2lem  40942  dvmptmulf  40945  dvxpaek  40948  dvmptfprod  40953  dvnprodlem2  40955  dvnprodlem3  40956  itgsin0pilem1  40958  itgsinexplem1  40962  itgsubsticclem  40983  stoweidlem13  41022  wallispilem4  41077  wallispi2lem1  41080  wallispi2lem2  41081  stirlinglem1  41083  dirkerper  41105  dirkertrigeqlem1  41107  dirkertrigeqlem3  41109  dirkertrigeq  41110  dirkeritg  41111  dirkercncflem1  41112  dirkercncflem2  41113  fourierdlem36  41152  fourierdlem41  41157  fourierdlem42  41158  fourierdlem48  41163  fourierdlem56  41171  fourierdlem57  41172  fourierdlem58  41173  fourierdlem60  41175  fourierdlem61  41176  fourierdlem62  41177  fourierdlem65  41180  fourierdlem73  41188  fourierdlem80  41195  fourierdlem87  41202  fourierdlem89  41204  fourierdlem90  41205  fourierdlem91  41206  fourierdlem100  41215  fourierdlem103  41218  fourierdlem107  41222  fourierdlem112  41227  fourierdlem113  41228  fourierdlem115  41230  fouriercnp  41235  sqwvfoura  41237  sqwvfourb  41238  fourierswlem  41239  fouriersw  41240  etransclem2  41245  etransclem37  41280  etransclem46  41289  hoidmvlelem3  41603  vonioolem2  41687  issmflem  41728  smfmullem2  41791  1t10e1p1e11  42206  prelrrx2  42277  fmtno0  42300  fmtno1  42301  fmtnorec2lem  42302  fmtnorec3  42308  fmtno2  42310  fmtno3  42311  fmtno4  42312  fmtno4sqrt  42331  fmtno4prmfac  42332  2exp5  42355  139prmALT  42359  31prm  42360  2exp7  42362  2exp11  42365  mod42tp1mod8  42367  lighneallem2  42371  5tcu2e40  42380  3exp4mod41  42381  41prothprmlem1  42382  41prothprmlem2  42383  41prothprm  42384  bits0ALTV  42438  sbgoldbo  42523  nnsum3primes4  42524  nnsum3primesgbe  42528  nnsum4primesodd  42532  nnsum4primesoddALTV  42533  nnsum4primeseven  42536  nnsum4primesevenALTV  42537  bgoldbtbndlem1  42541  tgoldbachlt  42552  2t6m3t4e0  42991  zlmodzxzequa  43150  zlmodzxznm  43151  zlmodzxzequap  43153  nn0sumshdiglemA  43278  nn0sumshdiglemB  43279  nn0sumshdiglem1  43280  2sphere  43315  line2  43318  sec0  43413  amgmw2d  43460