Theorem oveq2i 6661

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 6658	. 2 ⊢ (𝐴 = 𝐵 → (𝐶𝐹𝐴) = (𝐶𝐹𝐵))
3	1, 2	ax-mp 5	1 ⊢ (𝐶𝐹𝐴) = (𝐶𝐹𝐵)

Syntax hints:   = wceq 1483  (class class class)co 6650

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-rex 2918  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-iota 5851  df-fv 5896  df-ov 6653

This theorem is referenced by:  caov32  6861  caov4  6865  caov42  6867  seqomsuc  7552  oa1suc  7611  o2p2e4  7621  om1  7622  oe1  7624  oawordeulem  7634  oeoalem  7676  nnm1  7728  nnm2  7729  nneob  7732  omopthlem1  7735  mapsnconst  7903  mapsncnv  7904  map2xp  8130  cantnflt  8569  cnfcom2  8599  infxpenc  8841  infxpenc2  8845  ackbij1lem5  9046  alephom  9407  pwxpndom2  9487  adderpqlem  9776  addassnq  9780  mulcanenq  9782  distrnq  9783  ltanq  9793  ltexnq  9797  halfnq  9798  ltrnq  9801  archnq  9802  addclprlem2  9839  prlem934  9855  prlem936  9869  addcmpblnr  9890  mulcmpblnrlem  9891  ltsrpr  9898  m1p1sr  9913  m1m1sr  9914  0idsr  9918  1idsr  9919  00sr  9920  pn0sr  9922  recexsrlem  9924  mulgt0sr  9926  sqgt0sr  9927  mulresr  9960  axmulcom  9976  axmulass  9978  axdistr  9979  axi2m1  9980  ax1rid  9982  axcnre  9985  mul02lem1  10212  addid1  10216  negid  10328  negsub  10329  subneg  10330  negsubdii  10366  muleqadd  10671  crne0  11013  2p2e4  11144  3p2e5  11160  3p3e6  11161  4p2e6  11162  4p3e7  11163  4p4e8  11164  5p2e7  11165  5p3e8  11166  5p4e9  11167  5p5e10OLD  11168  6p2e8  11169  6p3e9  11170  6p4e10OLD  11171  7p2e9  11172  7p3e10OLD  11173  8p2e10OLD  11174  3t3e9  11180  8th4div3  11252  halfpm6th  11253  addltmul  11268  div4p1lem1div2  11287  nn0n0n1ge2  11358  nneo  11461  zeo  11463  numsuc  11511  numltc  11528  numsucc  11549  numma  11557  nummul1c  11562  decrmac  11577  decsubi  11583  decsubiOLD  11584  decmul1  11585  decmul10add  11593  decmul10addOLD  11594  6p5lem  11595  5p5e10  11596  6p4e10  11598  7p3e10  11603  8p2e10  11610  4t3lem  11631  9t11e99  11671  9t11e99OLD  11672  decbin2  11683  xmulmnf1  12106  fztp  12397  fzprval  12401  fztpval  12402  fzshftral  12428  fz0tp  12440  fz0to3un2pr  12441  fzo01  12550  fzo12sn  12551  fzo13pr  12552  fzo0to2pr  12553  fzo0to3tp  12554  fzo0to42pr  12555  fzo1to4tp  12556  fzosplitprm1  12578  quoremz  12654  quoremnn0ALT  12656  intfrac2  12657  intfracq  12658  sqval  12922  sqrecii  12946  sq4e2t8  12962  cu2  12963  i3  12966  i4  12967  binom2i  12974  binom3  12985  crreczi  12989  3dec  13050  sq10OLD  13051  3decOLD  13053  nn0opthlem1  13055  facp1  13065  faclbnd  13077  faclbnd2  13078  faclbnd4lem1  13080  faclbnd4lem4  13083  bcn1  13100  bcn2  13106  4bc3eq4  13115  4bc2eq6  13116  hashgadd  13166  hashxplem  13220  hashmap  13222  hashfun  13224  hashbclem  13236  fz1isolem  13245  ccatlid  13369  ccatrid  13370  ccats1val2  13404  ccat2s1p2  13406  wrdeqs1cat  13474  swrdccatin12lem3  13490  swrdccat3a  13494  cats1fvn  13603  cats1cat  13606  cats2cat  13607  s3fn  13656  swrds2  13685  reim0  13858  cji  13899  sqrtm1  14016  absi  14026  rddif  14080  iseraltlem2  14413  iseralt  14415  fsump1i  14500  fsummulc2  14516  incexclem  14568  incexc  14569  arisum2  14593  geoihalfsum  14614  mertenslem1  14616  mertens  14618  risefall0lem  14757  risefac1  14764  fallfac1  14765  fallfacfwd  14767  bpoly0  14781  bpoly1  14782  bpolydiflem  14785  bpoly2  14788  bpoly3  14789  bpoly4  14790  fsumcube  14791  ef0lem  14809  ege2le3  14820  eft0val  14842  ef4p  14843  efgt1p2  14844  efgt1p  14845  tanval2  14863  efival  14882  ef01bndlem  14914  sin01bnd  14915  cos01bnd  14916  cos1bnd  14917  cos2bnd  14918  rpnnen2lem11  14953  sqrt2irrlemOLD  14978  3dvdsdec  15054  3dvdsdecOLD  15055  3dvds2dec  15056  3dvds2decOLD  15057  odd2np1lem  15064  odd2np1  15065  oddp1even  15068  opoe  15087  divalglem5  15120  divalglem6  15121  bits0  15150  0bits  15161  gcdaddmlem  15245  6gcd4e2  15255  lcmneg  15316  3lcm2e6woprm  15328  6lcm4e12  15329  3prm  15406  3lcm2e6  15440  phiprm  15482  eulerthlem2  15487  prmdiv  15490  pythagtriplem12  15531  pythagtriplem14  15533  pcmpt  15596  pcfac  15603  prmpwdvds  15608  pockthi  15611  prmreclem2  15621  prmreclem6  15625  4sqlem5  15646  4sqlem13  15661  modxai  15772  mod2xnegi  15775  gcdi  15777  decexp2  15779  numexpp1  15782  numexp2x  15783  decsplit0b  15784  decsplit1  15786  decsplit  15787  decsplit0bOLD  15788  decsplit1OLD  15790  decsplitOLD  15791  2exp16  15797  prmlem0  15812  139prm  15831  163prm  15832  317prm  15833  631prm  15834  1259lem4  15841  1259lem5  15842  1259prm  15843  2503lem1  15844  2503lem2  15845  2503lem3  15846  2503prm  15847  4001lem1  15848  4001lem4  15851  ressinbas  15936  rcaninv  16454  rescfth  16597  xpccatid  16828  oduval  17130  oppgmnd  17784  psgnunilem2  17915  psgnunilem4  17917  psgnpmtr  17930  psgn0fv0  17931  psgnsn  17940  psgnprfval1  17942  lsmmod2  18089  efgi0  18133  efgi1  18134  efginvrel2  18140  efgsval2  18146  efgsp1  18150  efgredleme  18156  efgredlemc  18158  efgcpbllemb  18168  frgpnabllem1  18276  lt6abl  18296  gsumconstf  18335  gsum2dlem2  18370  pwsgsum  18378  fsfnn0gsumfsffz  18379  dprd0  18430  dprdf1  18432  dprd2da  18441  ablfac1lem  18467  pgpfac1lem3  18476  pgpfaclem1  18480  srgbinomlem4  18543  opprring  18631  mulgass3  18637  evlsval  19519  mpff  19533  ply1assa  19569  gsumply1subr  19604  ply1coe  19666  coe1fzgsumdlem  19671  coe1fzgsumd  19672  gsumply1eq  19675  evl1gsumdlem  19720  evl1gsumd  19721  xrsnsgrp  19782  znbas  19892  znzrh2  19894  dsmmval2  20080  frlmip  20117  matgsum  20243  madetsumid  20267  mdetrsca  20409  mdetrsca2  20410  mdettpos  20417  m2detleiblem2  20434  madugsum  20449  madurid  20450  cpmat  20514  pmatcollpwfi  20587  pmatcollpw3fi1lem1  20591  pm2mpval  20600  mp2pm2mplem5  20615  chpmat1dlem  20640  chpmat1d  20641  chpidmat  20652  cpmidpmat  20678  cpmadugsumfi  20682  chcoeffeqlem  20690  cayleyhamilton0  20694  cayleyhamiltonALT  20696  cayleyhamilton1  20697  restin  20970  imacmp  21200  conncompconn  21235  uptx  21428  cnpflf2  21804  tmdgsum2  21900  tsmsres  21947  tsmsf1o  21948  tsmsmhm  21949  prdsxmet  22174  resspwsds  22177  prdsxmslem2  22334  tngngpim  22463  metdcn2  22642  metdcn  22643  metdscn2  22660  iimulcn  22737  icchmeo  22740  xrhmeo  22745  cnrehmeo  22752  cnheiborlem  22753  evth  22758  evth2  22759  lebnumlem2  22761  reparphti  22797  pcoass  22824  pi1xfrcnv  22857  ipcau2  23033  minveclem4  23203  pjthlem1  23208  ovolunlem1a  23264  unmbl  23305  uniioombl  23357  iblitg  23535  dfitg  23536  itg0  23546  iblcnlem1  23554  itgcnlem  23556  itgabs  23601  limcdif  23640  limccnp  23655  limccnp2  23656  dvexp  23716  dvmptid  23720  dvmptc  23721  dvmptfsum  23738  dveflem  23742  dvsincos  23744  mvth  23755  dvlipcn  23757  dvivthlem1  23771  dvfsumle  23784  dvfsumlem2  23790  itgsubst  23812  tdeglem4  23820  tdeglem2  23821  plypf1  23968  plymullem1  23970  coesub  24013  dgrmulc  24027  fta1lem  24062  vieta1lem1  24065  vieta1lem2  24066  aalioulem4  24090  aaliou3lem3  24099  abelthlem2  24186  abelthlem8  24193  abelthlem9  24194  sinhalfpilem  24215  efhalfpi  24223  cospi  24224  efipi  24225  sin2pi  24227  cos2pi  24228  ef2pi  24229  sin2pim  24237  cos2pim  24238  sinmpi  24239  cosmpi  24240  sinppi  24241  cosppi  24242  sincosq4sgn  24253  tangtx  24257  sincos4thpi  24265  sincos6thpi  24267  sincos3rdpi  24268  pige3  24269  abssinper  24270  efif1olem4  24291  efifo  24293  eff1o  24295  circgrp  24298  circsubm  24299  logneg  24334  logimul  24360  logneg2  24361  dvrelog  24383  logcnlem4  24391  dvlog  24397  dvlog2  24399  logtayl  24406  1cxp  24418  ecxp  24419  cxpsqrt  24449  dvsqrt  24483  dvcnsqrt  24485  root1eq1  24496  cxpeq  24498  elogb  24508  ang180lem1  24539  ang180lem2  24540  heron  24565  1cubrlem  24568  1cubr  24569  dcubic2  24571  mcubic  24574  cubic2  24575  binom4  24577  dquartlem1  24578  dquartlem2  24579  dquart  24580  quart1lem  24582  quart1  24583  quartlem1  24584  asinsin  24619  asin1  24621  acos1  24622  atanlogsublem  24642  atanlogsub  24643  efiatan2  24644  2efiatan  24645  tanatan  24646  atanbnd  24653  atan1  24655  dvatan  24662  atantayl2  24665  leibpilem2  24668  leibpi  24669  log2cnv  24671  log2tlbnd  24672  log2ublem1  24673  log2ublem2  24674  log2ublem3  24675  log2ub  24676  birthday  24681  amgmlem  24716  emcllem5  24726  lgamgulmlem2  24756  lgamgulmlem5  24759  lgam1  24790  wilthlem2  24795  ftalem6  24804  basellem2  24808  basellem3  24809  basellem5  24811  basellem8  24814  cht1  24891  chp1  24893  1sgmprm  24924  ppiublem2  24928  ppiub  24929  chtublem  24936  chtub  24937  logfacbnd3  24948  bcp1ctr  25004  bclbnd  25005  bposlem1  25009  bposlem4  25012  bposlem6  25014  bposlem8  25016  bposlem9  25017  lgslem1  25022  lgsdir2lem1  25050  lgsdir2lem2  25051  lgsdir2lem3  25052  lgsdir2lem5  25054  lgs1  25066  gausslemma2dlem1a  25090  gausslemma2dlem3  25093  gausslemma2dlem4  25094  gausslemma2d  25099  lgseisenlem1  25100  lgseisenlem3  25102  lgsquadlem1  25105  lgsquadlem2  25106  lgsquad2lem2  25110  m1lgs  25113  2lgslem1a2  25115  2sqlem8  25151  2sqblem  25156  logdivsum  25222  mulog2sumlem2  25224  log2sumbnd  25233  selberglem1  25234  selberglem2  25235  pntrmax  25253  pntibndlem2  25280  pntibndlem3  25281  pntlemg  25287  pntlemr  25291  pntlemo  25296  ostth2lem3  25324  ostth2lem4  25325  istrkg3ld  25360  trgcgrg  25410  tgcgr4  25426  colperpexlem1  25622  ax5seglem7  25815  axlowdimlem4  25825  axlowdimlem16  25837  setsiedg  25928  vdegp1ci  26434  finsumvtxdg2sstep  26445  finsumvtxdg2size  26446  wlkp1lem6  26575  wlkp1lem8  26577  wlkp1  26578  uhgrwkspthlem2  26650  pthdlem1  26662  pthdlem2  26664  pthd  26665  crctcshwlkn0lem4  26705  crctcshwlkn0lem5  26706  crctcshwlkn0lem6  26707  crctcshlem4  26712  crctcshwlkn0  26713  2wlkdlem2  26822  2wlkdlem4  26824  2pthdlem1  26826  clwlkclwwlk2  26904  wwlksext2clwwlk  26924  0ewlk  26975  1ewlk  26976  0wlk  26977  1pthdlem1  26995  1pthdlem2  26996  1wlkdlem1  26997  1wlkdlem4  27000  wlk2v2e  27017  3wlkdlem2  27020  3wlkdlem4  27022  3pthdlem1  27024  eupth0  27074  eupthp1  27076  eucrctshift  27103  eucrct2eupth  27105  extwwlkfablem1  27207  numclwwlkovf2exlem1  27211  numclwlk1lem2foalem  27222  numclwlk2lem2f  27236  frgrregord013  27253  ex-exp  27307  ex-bc  27309  ex-gcd  27314  ex-lcm  27315  ex-ind-dvds  27318  smcnlem  27552  ipidsq  27565  dipcj  27569  dip0r  27572  nmlnoubi  27651  nmblolbii  27654  blocnilem  27659  ip1ilem  27681  ip2i  27683  ipdirilem  27684  ipasslem10  27694  ipasslem11  27695  siilem1  27706  hvmul0  27881  hvsubsub4i  27916  hvnegdii  27919  hvsubeq0i  27920  hvsubcan2i  27921  hvsubaddi  27923  hvsub0  27933  hisubcomi  27961  normlem0  27966  normlem1  27967  normlem2  27968  normlem3  27969  normlem9  27975  norm-ii-i  27994  norm3difi  28004  normpari  28011  polid2i  28014  polidi  28015  bcsiALT  28036  pjhthlem1  28250  chdmm3i  28338  chdmm4i  28339  chjidm  28379  chj4i  28382  chjjdiri  28383  spanunsni  28438  pjoml4i  28446  cmcm2i  28452  qlax4i  28489  qlax5i  28490  pjadjii  28533  pjmulii  28536  pjsubii  28537  pjssmii  28540  pjcji  28543  pjneli  28582  hoadd32i  28637  ho0subi  28654  hosubid1  28657  hosd2i  28682  hopncani  28683  hosubeq0i  28685  lnopeq0lem1  28864  lnopunilem1  28869  lnophmlem2  28876  nmbdoplbi  28883  nmcopexi  28886  lnfnmuli  28903  nmcfnexi  28910  nmoptri2i  28958  nmopcoadji  28960  golem1  29130  mdsl1i  29180  cvmdi  29183  mdslmd3i  29191  csmdsymi  29193  dfdec100  29576  dfdp2OLD  29579  dp20u  29585  dpmul10  29603  dpmul100  29605  dp3mul10  29606  dpmul1000  29607  dpexpp1  29616  0dp2dp  29617  dpmul  29621  dpmul4  29622  1mhdrd  29624  xrge00  29686  archirngz  29743  archiabllem2c  29749  gsumle  29779  gsummpt2co  29780  gsumvsca1  29782  gsumvsca2  29783  xrge0slmod  29844  psgnfzto1st  29855  lmat22det  29888  madjusmdetlem4  29896  raddcn  29975  xrge0iifhom  29983  xrge0mulc1cn  29987  cbvesum  30104  gsumesum  30121  esumpfinvallem  30136  esumpfinvalf  30138  dya2icoseg  30339  sitg0  30408  eulerpartlemd  30428  eulerpartlemgvv  30438  eulerpartlemgh  30440  fib0  30461  fib1  30462  fibp1  30463  orrvcval4  30526  orrvcoel  30527  orrvccel  30528  coinflipprob  30541  coinflippvt  30546  ballotlem2  30550  ballotth  30599  signstf0  30645  signstfvn  30646  signsvtn0  30647  signstfvp  30648  signstfveq0  30654  signsvf0  30657  signsvf1  30658  signsvfn  30659  signshf  30665  prodfzo03  30681  itgexpif  30684  repr0  30689  hgt750lemd  30726  hgt750lem  30729  hgt750lem2  30730  subfacp1lem1  31161  subfacp1lem5  31166  subfacval2  31169  subfaclim  31170  subfacval3  31171  cvxpconn  31224  cvxsconn  31225  mrsub0  31413  problem4  31562  quad3  31564  sinccvglem  31566  iexpire  31621  faclimlem1  31629  frrlem5  31784  fwddifnp1  32272  knoppcnlem10  32492  knoppndvlem7  32509  knoppndvlem21  32523  cnndvlem1  32528  finxpreclem4  33231  ptrest  33408  poimirlem27  33436  dvtan  33460  itgabsnc  33479  ftc1anclem8  33492  dvasin  33496  dvacos  33497  areacirclem1  33500  areacirclem4  33503  areacirc  33505  prdstotbnd  33593  prdsbnd2  33594  repwsmet  33633  rrnequiv  33634  reheibor  33638  dalem-cly  34957  pmodN  35136  cdleme0cp  35501  cdleme0cq  35502  cdleme1  35514  cdleme3d  35518  cdleme3h  35522  cdleme4  35525  cdleme5  35527  cdleme7a  35530  cdleme8  35537  cdleme9  35540  cdleme10  35541  cdleme11g  35552  cdleme15b  35562  cdleme21  35625  cdleme22e  35632  cdleme22eALTN  35633  cdleme23c  35639  cdleme25cv  35646  cdleme35b  35738  cdleme35c  35739  cdleme42a  35759  cdleme42d  35761  cdleme43aN  35777  cdlemeg46gfv  35818  cdlemk35  36200  dihjatcclem1  36707  lcdval2  36879  mapdpglem21  36981  mapfzcons  37279  mapfzcons1cl  37281  2rexfrabdioph  37360  3rexfrabdioph  37361  4rexfrabdioph  37362  6rexfrabdioph  37363  7rexfrabdioph  37364  rabdiophlem2  37366  diophren  37377  rabren3dioph  37379  pellexlem5  37397  pell1qr1  37435  rmspecfund  37474  jm2.17a  37527  jm2.17b  37528  jm2.27c  37574  jm2.27dlem5  37580  lmhmlnmsplit  37657  arearect  37801  areaquad  37802  relexp2  37969  trclfvdecomr  38020  k0004val0  38452  inductionexd  38453  unitadd  38498  amgm2d  38501  amgm3d  38502  lhe4.4ex1a  38528  expgrowthi  38532  expgrowth  38534  bccn1  38543  binomcxplemdvbinom  38552  binomcxplemdvsum  38554  binomcxplemnotnn0  38555  binomcxp  38556  refsumcn  39189  unirnmapsn  39406  oddfl  39489  infleinflem2  39587  sumnnodd  39862  cosnegpi  40078  dvcosre  40126  dvsinax  40127  ioodvbdlimc1lem2  40147  ioodvbdlimc2lem  40149  dvmptmulf  40152  dvxpaek  40155  dvmptfprod  40160  dvnprodlem2  40162  dvnprodlem3  40163  itgsin0pilem1  40165  itgsinexplem1  40169  itgsubsticclem  40191  stoweidlem13  40230  wallispilem4  40285  wallispi2lem1  40288  wallispi2lem2  40289  stirlinglem1  40291  dirkerper  40313  dirkertrigeqlem1  40315  dirkertrigeqlem3  40317  dirkertrigeq  40318  dirkeritg  40319  dirkercncflem1  40320  dirkercncflem2  40321  fourierdlem36  40360  fourierdlem41  40365  fourierdlem42  40366  fourierdlem48  40371  fourierdlem56  40379  fourierdlem57  40380  fourierdlem58  40381  fourierdlem60  40383  fourierdlem61  40384  fourierdlem62  40385  fourierdlem65  40388  fourierdlem73  40396  fourierdlem80  40403  fourierdlem87  40410  fourierdlem89  40412  fourierdlem90  40413  fourierdlem91  40414  fourierdlem100  40423  fourierdlem103  40426  fourierdlem107  40430  fourierdlem112  40435  fourierdlem113  40436  fourierdlem115  40438  fouriercnp  40443  sqwvfoura  40445  sqwvfourb  40446  fourierswlem  40447  fouriersw  40448  etransclem2  40453  etransclem37  40488  etransclem46  40497  hoidmvlelem3  40811  vonioolem2  40895  issmflem  40936  smfmullem2  40999  1t10e1p1e11  41319  1t10e1p1e11OLD  41320  pfx1  41411  pfxccatpfx1  41427  pfxccatpfx2  41428  fmtno0  41452  fmtno1  41453  fmtnorec2lem  41454  fmtnorec3  41460  fmtno2  41462  fmtno3  41463  fmtno4  41464  fmtno4sqrt  41483  fmtno4prmfac  41484  2exp5  41507  139prmALT  41511  31prm  41512  2exp7  41514  2exp11  41517  mod42tp1mod8  41519  lighneallem2  41523  5tcu2e40  41532  3exp4mod41  41533  41prothprmlem1  41534  41prothprmlem2  41535  41prothprm  41536  bits0ALTV  41590  sbgoldbo  41675  nnsum3primes4  41676  nnsum3primesgbe  41680  nnsum4primesodd  41684  nnsum4primesoddALTV  41685  nnsum4primeseven  41688  nnsum4primesevenALTV  41689  bgoldbtbndlem1  41693  tgoldbachlt  41704  tgoldbachltOLD  41710  2t6m3t4e0  42126  zlmodzxzequa  42285  zlmodzxznm  42286  zlmodzxzequap  42288  nn0sumshdiglemA  42413  nn0sumshdiglemB  42414  nn0sumshdiglem1  42415  sec0  42501  amgmw2d  42550