Theorem oveq2i 6560

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

Syntax hints:   = wceq 1475  (class class class)co 6549

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-rex 2902  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-br 4584  df-iota 5768  df-fv 5812  df-ov 6552

This theorem is referenced by:  caov32  6759  caov4  6763  caov42  6765  seqomsuc  7439  oa1suc  7498  o2p2e4  7508  om1  7509  oe1  7511  oawordeulem  7521  oeoalem  7563  nnm1  7615  nnm2  7616  nneob  7619  omopthlem1  7622  mapsnconst  7789  mapsncnv  7790  map2xp  8015  cantnflt  8452  cnfcom2  8482  infxpenc  8724  infxpenc2  8728  ackbij1lem5  8929  alephom  9286  pwxpndom2  9366  adderpqlem  9655  addassnq  9659  mulcanenq  9661  distrnq  9662  ltanq  9672  ltexnq  9676  halfnq  9677  ltrnq  9680  archnq  9681  addclprlem2  9718  prlem934  9734  prlem936  9748  addcmpblnr  9769  mulcmpblnrlem  9770  ltsrpr  9777  m1p1sr  9792  m1m1sr  9793  0idsr  9797  1idsr  9798  00sr  9799  pn0sr  9801  recexsrlem  9803  mulgt0sr  9805  sqgt0sr  9806  mulresr  9839  axmulcom  9855  axmulass  9857  axdistr  9858  axi2m1  9859  ax1rid  9861  axcnre  9864  mul02lem1  10091  addid1  10095  negid  10207  negsub  10208  subneg  10209  negsubdii  10245  muleqadd  10550  crne0  10890  2p2e4  11021  3p2e5  11037  3p3e6  11038  4p2e6  11039  4p3e7  11040  4p4e8  11041  5p2e7  11042  5p3e8  11043  5p4e9  11044  5p5e10OLD  11045  6p2e8  11046  6p3e9  11047  6p4e10OLD  11048  7p2e9  11049  7p3e10OLD  11050  8p2e10OLD  11051  3t3e9  11057  8th4div3  11129  halfpm6th  11130  addltmul  11145  div4p1lem1div2  11164  nn0n0n1ge2  11235  nneo  11337  zeo  11339  numsuc  11387  numltc  11404  numsucc  11425  numma  11433  nummul1c  11438  decrmac  11453  decsubi  11459  decsubiOLD  11460  decmul1  11461  decmul10add  11469  decmul10addOLD  11470  6p5lem  11471  5p5e10  11472  6p4e10  11474  7p3e10  11479  8p2e10  11486  4t3lem  11507  9t11e99  11547  9t11e99OLD  11548  decbin2  11559  xmulmnf1  11978  fztp  12267  fzprval  12271  fztpval  12272  fzshftral  12297  fz0tp  12309  fz0to3un2pr  12310  fzo01  12417  fzo12sn  12418  fzo13pr  12419  fzo0to2pr  12420  fzo0to3tp  12421  fzo0to42pr  12422  fzo1to4tp  12423  quoremz  12516  quoremnn0ALT  12518  intfrac2  12519  intfracq  12520  sqval  12784  sqrecii  12808  sq4e2t8  12824  cu2  12825  i3  12828  i4  12829  binom2i  12836  binom3  12847  crreczi  12851  3dec  12912  sq10OLD  12913  3decOLD  12915  nn0opthlem1  12917  facp1  12927  faclbnd  12939  faclbnd2  12940  faclbnd4lem1  12942  faclbnd4lem4  12945  bcn1  12962  bcn2  12968  4bc3eq4  12977  4bc2eq6  12978  hashgadd  13027  hashxplem  13080  hashmap  13082  hashfun  13084  hashbclem  13093  fz1isolem  13102  ccatlid  13222  ccatrid  13223  ccats1val2  13256  ccat2s1p2  13258  wrdeqs1cat  13326  swrdccatin12lem3  13341  swrdccat3a  13345  cats1fvn  13454  cats1cat  13457  cats2cat  13458  s3fn  13506  swrds2  13533  reim0  13706  cji  13747  sqrtm1  13864  absi  13874  rddif  13928  iseraltlem2  14261  iseralt  14263  fsump1i  14342  fsummulc2  14358  incexclem  14407  incexc  14408  arisum2  14432  geoihalfsum  14453  mertenslem1  14455  mertens  14457  risefall0lem  14596  risefac1  14603  fallfac1  14604  fallfacfwd  14606  bpoly0  14620  bpoly1  14621  bpolydiflem  14624  bpoly2  14627  bpoly3  14628  bpoly4  14629  fsumcube  14630  ef0lem  14648  ege2le3  14659  eft0val  14681  ef4p  14682  efgt1p2  14683  efgt1p  14684  tanval2  14702  efival  14721  ef01bndlem  14753  sin01bnd  14754  cos01bnd  14755  cos1bnd  14756  cos2bnd  14757  rpnnen2lem11  14792  sqr2irrlem  14816  3dvdsdec  14892  3dvdsdecOLD  14893  3dvds2dec  14894  3dvds2decOLD  14895  odd2np1lem  14902  odd2np1  14903  oddp1even  14906  opoe  14925  divalglem5  14958  divalglem6  14959  bits0  14988  0bits  14999  gcdaddmlem  15083  6gcd4e2  15093  lcmneg  15154  3lcm2e6woprm  15166  6lcm4e12  15167  3prm  15244  3lcm2e6  15278  phiprm  15320  eulerthlem2  15325  prmdiv  15328  pythagtriplem12  15369  pythagtriplem14  15371  pcmpt  15434  pcfac  15441  prmpwdvds  15446  pockthi  15449  prmreclem2  15459  prmreclem6  15463  4sqlem5  15484  4sqlem13  15499  modxai  15610  mod2xnegi  15613  gcdi  15615  decexp2  15617  numexpp1  15620  numexp2x  15621  decsplit0b  15622  decsplit1  15624  decsplit  15625  decsplit0bOLD  15626  decsplit1OLD  15628  decsplitOLD  15629  2exp16  15635  prmlem0  15650  139prm  15669  163prm  15670  317prm  15671  631prm  15672  1259lem4  15679  1259lem5  15680  1259prm  15681  2503lem1  15682  2503lem2  15683  2503lem3  15684  2503prm  15685  4001lem1  15686  4001lem4  15689  ressinbas  15763  rcaninv  16277  rescfth  16420  xpccatid  16651  oduval  16953  oppgmnd  17607  psgnunilem2  17738  psgnunilem4  17740  psgnpmtr  17753  psgn0fv0  17754  psgnsn  17763  psgnprfval1  17765  lsmmod2  17912  efgi0  17956  efgi1  17957  efginvrel2  17963  efgsval2  17969  efgsp1  17973  efgredleme  17979  efgredlemc  17981  efgcpbllemb  17991  frgpnabllem1  18099  lt6abl  18119  gsumconstf  18158  gsum2dlem2  18193  pwsgsum  18201  fsfnn0gsumfsffz  18202  dprd0  18253  dprdf1  18255  dprd2da  18264  ablfac1lem  18290  pgpfac1lem3  18299  pgpfaclem1  18303  srgbinomlem4  18366  opprring  18454  mulgass3  18460  evlsval  19340  mpff  19354  ply1assa  19390  gsumply1subr  19425  ply1coe  19487  coe1fzgsumdlem  19492  coe1fzgsumd  19493  gsumply1eq  19496  evl1gsumdlem  19541  evl1gsumd  19542  xrsnsgrp  19601  znbas  19711  znzrh2  19713  dsmmval2  19899  frlmip  19936  matgsum  20062  madetsumid  20086  mdetrsca  20228  mdetrsca2  20229  mdettpos  20236  m2detleiblem2  20253  madugsum  20268  madurid  20269  cpmat  20333  pmatcollpwfi  20406  pmatcollpw3fi1lem1  20410  pm2mpval  20419  mp2pm2mplem5  20434  chpmat1dlem  20459  chpmat1d  20460  chpidmat  20471  cpmidpmat  20497  cpmadugsumfi  20501  chcoeffeqlem  20509  cayleyhamilton0  20513  cayleyhamiltonALT  20515  cayleyhamilton1  20516  restin  20780  imacmp  21010  concompcon  21045  uptx  21238  cnpflf2  21614  tmdgsum2  21710  tsmsres  21757  tsmsf1o  21758  tsmsmhm  21759  prdsxmet  21984  resspwsds  21987  prdsxmslem2  22144  tngngpim  22273  metdcn2  22450  metdcn  22451  metdscn2  22468  iimulcn  22545  icchmeo  22548  xrhmeo  22553  cnrehmeo  22560  cnheiborlem  22561  evth  22566  evth2  22567  lebnumlem2  22569  reparphti  22605  pcoass  22632  pi1xfrcnv  22665  ipcau2  22841  minveclem4  23011  pjthlem1  23016  ovolunlem1a  23071  unmbl  23112  uniioombl  23163  iblitg  23341  dfitg  23342  itg0  23352  iblcnlem1  23360  itgcnlem  23362  itgabs  23407  limcdif  23446  limccnp  23461  limccnp2  23462  dvexp  23522  dvmptid  23526  dvmptc  23527  dvmptfsum  23542  dveflem  23546  dvsincos  23548  mvth  23559  dvlipcn  23561  dvivthlem1  23575  dvfsumle  23588  dvfsumlem2  23594  itgsubst  23616  tdeglem4  23624  tdeglem2  23625  plypf1  23772  plymullem1  23774  coesub  23817  dgrmulc  23831  fta1lem  23866  vieta1lem1  23869  vieta1lem2  23870  aalioulem4  23894  aaliou3lem3  23903  abelthlem2  23990  abelthlem8  23997  abelthlem9  23998  sinhalfpilem  24019  efhalfpi  24027  cospi  24028  efipi  24029  sin2pi  24031  cos2pi  24032  ef2pi  24033  sin2pim  24041  cos2pim  24042  sinmpi  24043  cosmpi  24044  sinppi  24045  cosppi  24046  sincosq4sgn  24057  tangtx  24061  sincos4thpi  24069  sincos6thpi  24071  sincos3rdpi  24072  pige3  24073  abssinper  24074  efif1olem4  24095  efifo  24097  eff1o  24099  circgrp  24102  circsubm  24103  logneg  24138  logimul  24164  logneg2  24165  dvrelog  24183  logcnlem4  24191  dvlog  24197  dvlog2  24199  logtayl  24206  1cxp  24218  ecxp  24219  cxpsqrt  24249  dvsqrt  24283  dvcnsqrt  24285  root1eq1  24296  cxpeq  24298  elogb  24308  ang180lem1  24339  ang180lem2  24340  heron  24365  1cubrlem  24368  1cubr  24369  dcubic2  24371  mcubic  24374  cubic2  24375  binom4  24377  dquartlem1  24378  dquartlem2  24379  dquart  24380  quart1lem  24382  quart1  24383  quartlem1  24384  asinsin  24419  asin1  24421  acos1  24422  atanlogsublem  24442  atanlogsub  24443  efiatan2  24444  2efiatan  24445  tanatan  24446  atanbnd  24453  atan1  24455  dvatan  24462  atantayl2  24465  leibpilem2  24468  leibpi  24469  log2cnv  24471  log2tlbnd  24472  log2ublem1  24473  log2ublem2  24474  log2ublem3  24475  log2ub  24476  birthday  24481  amgmlem  24516  emcllem5  24526  lgamgulmlem2  24556  lgamgulmlem5  24559  lgam1  24590  wilthlem2  24595  ftalem6  24604  basellem2  24608  basellem3  24609  basellem5  24611  basellem8  24614  cht1  24691  chp1  24693  1sgmprm  24724  ppiublem2  24728  ppiub  24729  chtublem  24736  chtub  24737  logfacbnd3  24748  bcp1ctr  24804  bclbnd  24805  bposlem1  24809  bposlem4  24812  bposlem6  24814  bposlem8  24816  bposlem9  24817  lgslem1  24822  lgsdir2lem1  24850  lgsdir2lem2  24851  lgsdir2lem3  24852  lgsdir2lem5  24854  lgs1  24866  gausslemma2dlem1a  24890  gausslemma2dlem3  24893  gausslemma2dlem4  24894  gausslemma2d  24899  lgseisenlem1  24900  lgseisenlem3  24902  lgsquadlem1  24905  lgsquadlem2  24906  lgsquad2lem2  24910  m1lgs  24913  2lgslem1a2  24915  2sqlem8  24951  2sqblem  24956  logdivsum  25022  mulog2sumlem2  25024  log2sumbnd  25033  selberglem1  25034  selberglem2  25035  pntrmax  25053  pntibndlem2  25080  pntibndlem3  25081  pntlemg  25087  pntlemr  25091  pntlemo  25096  ostth2lem3  25124  ostth2lem4  25125  istrkg3ld  25160  trgcgrg  25210  tgcgr4  25226  colperpexlem1  25422  ax5seglem7  25615  axlowdimlem4  25625  axlowdimlem16  25637  uhgrstrrepe  25745  0wlk  26075  0trl  26076  wlkntrllem2  26090  wlkntrl  26092  constr1trl  26118  1pthonlem1  26119  constr2wlk  26128  constr2trl  26129  wlkdvspthlem  26137  constr3trllem3  26180  constr3trllem4  26181  constr3trllem5  26182  constr3pthlem1  26183  constr3pthlem3  26185  clwwlkn2  26303  clwlkisclwwlk2  26318  wwlkext2clwwlk  26331  vdgr1c  26432  nbhashuvtx1  26442  vdegp1ai  26511  vdegp1bi  26512  vdegp1ci  26513  extwwlkfablem2  26605  numclwwlkovf2ex  26613  numclwlk2lem2f  26630  frgraregord013  26645  ex-exp  26699  ex-bc  26701  ex-gcd  26706  ex-lcm  26707  ex-ind-dvds  26710  smcnlem  26936  ipidsq  26949  dipcj  26953  dip0r  26956  nmlnoubi  27035  nmblolbii  27038  blocnilem  27043  ip1ilem  27065  ip2i  27067  ipdirilem  27068  ipasslem10  27078  ipasslem11  27079  siilem1  27090  hvmul0  27265  hvsubsub4i  27300  hvnegdii  27303  hvsubeq0i  27304  hvsubcan2i  27305  hvsubaddi  27307  hvsub0  27317  hisubcomi  27345  normlem0  27350  normlem1  27351  normlem2  27352  normlem3  27353  normlem9  27359  norm-ii-i  27378  norm3difi  27388  normpari  27395  polid2i  27398  polidi  27399  bcsiALT  27420  pjhthlem1  27634  chdmm3i  27722  chdmm4i  27723  chjidm  27763  chj4i  27766  chjjdiri  27767  spanunsni  27822  pjoml4i  27830  cmcm2i  27836  qlax4i  27873  qlax5i  27874  pjadjii  27917  pjmulii  27920  pjsubii  27921  pjssmii  27924  pjcji  27927  pjneli  27966  hoadd32i  28021  ho0subi  28038  hosubid1  28041  hosd2i  28066  hopncani  28067  hosubeq0i  28069  lnopeq0lem1  28248  lnopunilem1  28253  lnophmlem2  28260  nmbdoplbi  28267  nmcopexi  28270  lnfnmuli  28287  nmcfnexi  28294  nmoptri2i  28342  nmopcoadji  28344  golem1  28514  mdsl1i  28564  cvmdi  28567  mdslmd3i  28575  csmdsymi  28577  xrge00  29017  archirngz  29074  archiabllem2c  29080  gsumle  29110  gsummpt2co  29111  gsumvsca1  29113  gsumvsca2  29114  xrge0slmod  29175  psgnfzto1st  29186  lmat22det  29216  madjusmdetlem4  29224  raddcn  29303  xrge0iifhom  29311  xrge0mulc1cn  29315  cbvesum  29431  gsumesum  29448  esumpfinvallem  29463  esumpfinvalf  29465  dya2icoseg  29666  sitg0  29735  eulerpartlemd  29755  eulerpartlemgvv  29765  eulerpartlemgh  29767  fib0  29788  fib1  29789  fibp1  29790  orrvcval4  29853  orrvcoel  29854  orrvccel  29855  coinflipprob  29868  coinflippvt  29873  ballotlem2  29877  ballotth  29926  signstf0  29971  signstfvn  29972  signsvtn0  29973  signstfvp  29974  signstfveq0  29980  signsvf0  29983  signsvf1  29984  signsvfn  29985  signshf  29991  subfacp1lem1  30415  subfacp1lem5  30420  subfacval2  30423  subfaclim  30424  subfacval3  30425  cvxpcon  30478  cvxscon  30479  mrsub0  30667  problem4  30816  quad3  30818  sinccvglem  30820  iexpire  30874  faclimlem1  30882  frrlem5  31028  fwddifnp1  31442  knoppcnlem10  31662  knoppndvlem7  31679  knoppndvlem21  31693  cnndvlem1  31698  finxpreclem4  32407  ptrest  32578  poimirlem27  32606  dvtan  32630  itgabsnc  32649  ftc1anclem8  32662  dvasin  32666  dvacos  32667  areacirclem1  32670  areacirclem4  32673  areacirc  32675  prdstotbnd  32763  prdsbnd2  32764  repwsmet  32803  rrnequiv  32804  reheibor  32808  dalem-cly  33975  pmodN  34154  cdleme0cp  34519  cdleme0cq  34520  cdleme1  34532  cdleme3d  34536  cdleme3h  34540  cdleme4  34543  cdleme5  34545  cdleme7a  34548  cdleme8  34555  cdleme9  34558  cdleme10  34559  cdleme11g  34570  cdleme15b  34580  cdleme21  34643  cdleme22e  34650  cdleme22eALTN  34651  cdleme23c  34657  cdleme25cv  34664  cdleme35b  34756  cdleme35c  34757  cdleme42a  34777  cdleme42d  34779  cdleme43aN  34795  cdlemeg46gfv  34836  cdlemk35  35218  dihjatcclem1  35725  lcdval2  35897  mapdpglem21  35999  mapfzcons  36297  mapfzcons1cl  36299  2rexfrabdioph  36378  3rexfrabdioph  36379  4rexfrabdioph  36380  6rexfrabdioph  36381  7rexfrabdioph  36382  rabdiophlem2  36384  diophren  36395  rabren3dioph  36397  pellexlem5  36415  pell1qr1  36453  rmspecfund  36492  jm2.17a  36545  jm2.17b  36546  jm2.27c  36592  jm2.27dlem5  36598  lmhmlnmsplit  36675  arearect  36820  areaquad  36821  relexp2  36988  trclfvdecomr  37039  k0004val0  37472  inductionexd  37473  unitadd  37520  amgm2d  37523  amgm3d  37524  lhe4.4ex1a  37550  expgrowthi  37554  expgrowth  37556  bccn1  37565  binomcxplemdvbinom  37574  binomcxplemdvsum  37576  binomcxplemnotnn0  37577  binomcxp  37578  refsumcn  38212  unirnmapsn  38401  oddfl  38430  infleinflem2  38528  sumnnodd  38697  cosnegpi  38750  dvcosre  38799  dvsinax  38801  ioodvbdlimc1lem2  38822  ioodvbdlimc2lem  38824  dvmptmulf  38827  dvxpaek  38830  dvmptfprod  38835  dvnprodlem2  38837  dvnprodlem3  38838  itgsin0pilem1  38841  itgsinexplem1  38845  itgsubsticclem  38867  stoweidlem13  38906  wallispilem4  38961  wallispi2lem1  38964  wallispi2lem2  38965  stirlinglem1  38967  dirkerper  38989  dirkertrigeqlem1  38991  dirkertrigeqlem3  38993  dirkertrigeq  38994  dirkeritg  38995  dirkercncflem1  38996  dirkercncflem2  38997  fourierdlem36  39036  fourierdlem41  39041  fourierdlem42  39042  fourierdlem48  39047  fourierdlem56  39055  fourierdlem57  39056  fourierdlem58  39057  fourierdlem60  39059  fourierdlem61  39060  fourierdlem62  39061  fourierdlem65  39064  fourierdlem73  39072  fourierdlem80  39079  fourierdlem87  39086  fourierdlem89  39088  fourierdlem90  39089  fourierdlem91  39090  fourierdlem100  39099  fourierdlem103  39102  fourierdlem107  39106  fourierdlem112  39111  fourierdlem113  39112  fourierdlem115  39114  fouriercnp  39119  sqwvfoura  39121  sqwvfourb  39122  fourierswlem  39123  fouriersw  39124  etransclem2  39129  etransclem37  39164  etransclem46  39173  hoidmvlelem3  39487  vonioolem2  39572  issmflem  39613  smfmullem2  39677  1t10e1p1e11  39937  1t10e1p1e11OLD  39938  fmtno0  39990  fmtno1  39991  fmtnorec2lem  39992  fmtnorec3  39998  fmtno2  40000  fmtno3  40001  fmtno4  40002  fmtno4sqrt  40021  fmtno4prmfac  40022  2exp5  40045  139prmALT  40049  31prm  40050  2exp7  40052  2exp11  40055  mod42tp1mod8  40057  lighneallem2  40061  5tcu2e40  40070  3exp4mod41  40071  41prothprmlem1  40072  41prothprmlem2  40073  41prothprm  40074  bits0ALTV  40128  nnsum3primes4  40204  nnsum3primesgbe  40208  nnsum4primesodd  40212  nnsum4primesoddALTV  40213  nnsum4primeseven  40216  nnsum4primesevenALTV  40217  bgoldbtbndlem1  40221  tgoldbachlt  40230  tgoldbachltOLD  40237  pfx1  40274  pfxccatpfx1  40290  pfxccatpfx2  40291  vdegp1ci-av  40754  1wlkp1lem6  40887  1wlkp1lem8  40889  1wlkp1  40890  uhgr1wlkspthlem2  40960  pthdlem1  40972  pthdlem2  40974  pthd  40975  crctcsh1wlkn0lem4  41016  crctcsh1wlkn0lem5  41017  crctcsh1wlkn0lem6  41018  crctcshlem4  41023  crctcsh1wlkn0  41024  21wlkdlem2  41133  21wlkdlem4  41135  2pthdlem1  41137  clwlkclwwlk2  41212  wwlksext2clwwlk  41231  0ewlk  41282  1ewlk  41283  01wlk  41284  1pthdlem1  41302  1pthdlem2  41303  11wlkdlem1  41304  11wlkdlem4  41307  1wlk2v2e  41324  31wlkdlem2  41327  31wlkdlem4  41329  3pthdlem1  41331  eupth0  41382  eupthp1  41384  eucrctshift  41411  eucrct2eupth  41413  av-extwwlkfablem1  41508  av-extwwlkfablem2  41510  av-numclwwlkovf2ex  41517  av-numclwlk2lem2f  41533  av-frgraregord013  41549  2t6m3t4e0  41919  zlmodzxzequa  42079  zlmodzxznm  42080  zlmodzxzequap  42082  nn0sumshdiglemA  42211  nn0sumshdiglemB  42212  nn0sumshdiglem1  42213  sec0  42300  dfdp2OLD  42307  amgmw2d  42359