Theorem oveq1i 7262

Description: Equality inference for operation value. (Contributed by NM, 28-Feb-1995.)

Hypothesis

Ref	Expression
oveq1i.1	⊢ 𝐴 = 𝐵

Assertion

Ref	Expression
oveq1i	⊢ (𝐴𝐹𝐶) = (𝐵𝐹𝐶)

Proof of Theorem oveq1i

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

Syntax hints:   = wceq 1543  (class class class)co 7252

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2114  ax-9 2122  ax-ext 2710

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-sb 2073  df-clab 2717  df-cleq 2731  df-clel 2818  df-rab 3073  df-v 3425  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-nul 4255  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-iota 6373  df-fv 6423  df-ov 7255

This theorem is referenced by:  caov12  7475  caov411  7479  omopthlem1  8426  map1  8761  pw2eng  8795  fsuppunbi  9054  cnfcomlem  9362  cnfcom2  9365  infxpenc2  9684  adderpqlem  10616  addassnq  10620  distrnq  10623  halfnq  10638  archnq  10642  addclprlem2  10679  addcmpblnr  10731  ltsrpr  10739  m1m1sr  10755  recexsrlem  10765  sqgt0sr  10768  map2psrpr  10772  axi2m1  10821  axcnre  10826  mul02lem2  11057  addid1  11060  cnegex2  11062  addid2  11063  mvrraddi  11143  mvlladdi  11144  negsubdi  11182  mulneg1  11316  recextlem1  11510  recdiv  11586  divmul13i  11641  mvllmuli  11713  2p2e4  12013  2times  12014  1p2e3  12021  3p2e5  12029  3p3e6  12030  4p2e6  12031  4p3e7  12032  4p4e8  12033  5p2e7  12034  5p3e8  12035  5p4e9  12036  6p2e8  12037  6p3e9  12038  7p2e9  12039  1mhlfehlf  12097  8th4div3  12098  halfpm6th  12099  nneo  12309  9p1e10  12343  dfdec10  12344  num0h  12353  numsuc  12355  dec10p  12384  numma  12385  nummac  12386  numma2c  12387  numadd  12388  numaddc  12389  nummul2c  12391  decaddci  12402  decsubi  12404  5p5e10  12412  6p4e10  12413  7p3e10  12416  8p2e10  12421  decbin0  12481  decbin2  12482  xmulm1  12919  xadddi2  12935  x2times  12937  elfzp1b  13237  elfzm1b  13238  fz1ssfz0  13256  fz0to4untppr  13263  fz0sn0fz1  13277  fz0add1fz1  13360  elfz0lmr  13405  fldiv4p1lem1div2  13458  quoremz  13478  quoremnn0ALT  13480  uzrdgxfr  13590  mulexpz  13726  expaddz  13730  sqrecii  13803  sq4e2t8  13819  cu2  13820  i3  13823  iexpcyc  13826  binom2i  13831  binom3  13842  crreczi  13846  discr  13858  3dec  13883  nn0opthlem1  13885  nn0opth2i  13888  faclbnd  13907  bcp1nk  13934  bcpasc  13938  hashp1i  14021  hashxplem  14051  hashpw  14054  hashfun  14055  hashbc  14068  ccatlid  14194  pfxccatin12lem2c  14346  revs1  14381  cats1cat  14477  cats2cat  14478  lsws2  14520  lsws3  14521  lsws4  14522  s3s4  14549  s2s5  14550  s5s2  14551  imre  14722  crim  14729  remullem  14742  cnpart  14854  sqrtneglem  14881  absexpz  14920  absimle  14924  sqreulem  14974  amgm2  14984  iseraltlem2  15297  iseraltlem3  15298  modfsummod  15409  binomlem  15444  binom11  15447  arisum  15475  arisum2  15476  pwdif  15483  georeclim  15487  geo2sum  15488  mertenslem1  15499  mertens  15501  prodfrec  15510  fprodm1s  15583  fprodp1s  15584  fprodmodd  15610  fallfacfwd  15649  0risefac  15651  bpolydiflem  15667  bpoly2  15670  bpoly3  15671  bpoly4  15672  fsumcube  15673  efzval  15714  resinval  15747  recosval  15748  efi4p  15749  tan0  15763  efival  15764  sinhval  15766  coshval  15767  cosadd  15777  cos2tsin  15791  ef01bndlem  15796  cos1bnd  15799  cos2bnd  15800  absefib  15810  efieq1re  15811  demoivreALT  15813  eirrlem  15816  rpnnen2lem3  15828  rpnnen2lem11  15836  ruclem7  15848  3dvds  15943  3dvdsdec  15944  3dvds2dec  15945  odd2np1  15953  nn0o1gt2  15993  nn0o  15995  pwp1fsum  16003  divalglem2  16007  divalglem9  16013  flodddiv4  16025  m1bits  16050  sadcp1  16065  sadeq  16082  smupp1  16090  smumul  16103  gcdaddmlem  16134  3lcm2e6woprm  16223  nn0gcdsq  16359  phiprmpw  16380  prmdiv  16389  prmdiveq  16390  pythagtriplem1  16420  pythagtriplem12  16430  pythagtriplem14  16432  pockthi  16511  infpnlem1  16514  prmreclem4  16523  4sqlem12  16560  4sqlem13  16561  4sqlem19  16567  vdwapun  16578  vdwlem6  16590  0hashbc  16611  prmo2  16644  prmo3  16645  dec5dvds  16668  dec5nprm  16670  dec2nprm  16671  modxai  16672  modxp1i  16674  mod2xnegi  16675  modsubi  16676  gcdmodi  16678  decexp2  16679  decsplit0b  16684  decsplit1  16686  decsplit  16687  karatsuba  16688  2exp7  16692  2exp8  16693  3exp3  16696  5prm  16713  7prm  16715  11prm  16719  prmlem2  16724  37prm  16725  43prm  16726  83prm  16727  139prm  16728  163prm  16729  317prm  16730  631prm  16731  prmo5  16733  1259lem1  16735  1259lem2  16736  1259lem3  16737  1259lem4  16738  1259lem5  16739  2503lem1  16741  2503lem2  16742  2503lem3  16743  2503prm  16744  4001lem1  16745  4001lem2  16746  4001lem3  16747  4001lem4  16748  4001prm  16749  pwsbas  17090  rcaninv  17398  subsubc  17459  xpccatid  17796  subsubm  18345  smndex2dnrinv  18444  mulg2  18603  subsubg  18668  oppgmnd  18851  gsumwrev  18863  psgnunilem2  18993  sylow1lem1  19093  subgslw  19111  sylow3  19128  efginvrel2  19223  efgsfo  19235  frgpnabllem1  19364  gsumzaddlem  19412  gsummptfzsplitl  19424  gsummpt1n0  19456  dprdfid  19510  ablfac1lem  19561  pgpfac1lem3  19570  pgpfaclem1  19574  ablsimpgfindlem1  19600  mgpress  19625  mgpressOLD  19626  srgbinomlem4  19669  opprring  19763  unitsubm  19802  subsubrg  19940  cntzsdrg  19960  subdrgint  19961  lsslss  20113  xrsnsgrp  20521  gzrngunit  20551  expghm  20584  chrid  20618  zrhpsgnmhm  20676  psgndiflemA  20693  frlmip  20870  frlmphl  20873  evlsval  21181  mpff  21199  coe1fzgsumdlem  21357  evl1gsumdlem  21407  matvsca2  21460  mattposvs  21487  m2detleiblem3  21661  m2detleiblem4  21662  cpmidpmat  21905  resstopn  22220  cnmpt1res  22710  ressuss  23297  iscusp2  23337  ucnextcn  23339  txmetcnp  23584  rerest  23848  xrtgioo  23850  xrrest  23851  cnmpopc  23972  xrhmeo  23990  clmvs2  24138  clmnegneg  24148  ncvsm1  24198  ncvspi  24200  cphassir  24259  cphipval2  24285  reust  24425  rrxprds  24433  csbren  24443  rrxdsfi  24455  minveclem2  24470  ovolunlem1a  24540  ovolicc2lem4  24564  uniioombllem5  24631  iblabs  24873  iblabsr  24874  iblmulc2  24875  itgmulc2  24878  limcres  24930  dvfval  24941  dvreslem  24953  dvres2lem  24954  dvcnp2  24964  cpnres  24981  dvcobr  24990  dveflem  25023  lhop1lem  25057  lhop2  25059  dvcnvrelem2  25062  plyun0  25238  coeeulem  25265  coeeu  25266  dvply1  25324  dvtaylp  25409  taylthlem2  25413  taylth  25414  dvradcnv  25460  pserdvlem2  25467  abelthlem8  25478  abelth  25480  sinhalfpilem  25500  cospi  25509  eulerid  25511  cos2pi  25513  ef2kpi  25515  sinhalfpip  25529  sinhalfpim  25530  coshalfpip  25531  coshalfpim  25532  sincosq3sgn  25537  sincosq4sgn  25538  tangtx  25542  sincos4thpi  25550  sincos6thpi  25552  sineq0  25560  tanregt0  25575  logm1  25624  abslogle  25653  tanarg  25654  logcnlem4  25680  advlogexp  25690  cxpsqrt  25738  dvsqrt  25775  dvcnsqrt  25777  cxpcn3  25781  root1cj  25789  cxpeq  25790  logb1  25799  2logb9irr  25825  sqrt2cxp2logb9e3  25829  ang180lem1  25839  ang180lem2  25840  ang180lem3  25841  lawcos  25846  isosctrlem1  25848  isosctrlem2  25849  quad2  25869  1cubrlem  25871  1cubr  25872  dcubic2  25874  mcubic  25877  binom4  25880  dquartlem1  25881  quart1lem  25885  quart1  25886  quartlem1  25887  asinlem  25898  asinlem2  25899  asinlem3a  25900  acosneg  25917  efiasin  25918  asinsinlem  25921  asinsin  25922  acoscos  25923  asin1  25924  acosbnd  25930  atancj  25940  efiatan  25942  atanlogaddlem  25943  efiatan2  25947  2efiatan  25948  tanatan  25949  cosatan  25951  atantan  25953  atanbndlem  25955  atans2  25961  dvatan  25965  atantayl  25967  atantayl2  25968  log2cnv  25974  log2tlbnd  25975  log2ublem2  25977  log2ublem3  25978  log2ub  25979  birthday  25984  jensenlem1  26016  amgmlem  26019  lgamgulmlem2  26059  lgamgulmlem5  26062  lgambdd  26066  ftalem2  26103  ftalem5  26106  ftalem6  26107  basellem2  26111  basellem3  26112  basellem5  26114  basellem8  26117  basellem9  26118  mule1  26177  ppi1i  26197  musum  26220  ppiublem1  26230  ppiub  26232  chtublem  26239  chtub  26240  dchrptlem1  26292  dchrptlem2  26293  bclbnd  26308  bposlem6  26317  bposlem8  26319  bposlem9  26320  lgsdir2lem1  26353  lgsdir2lem2  26354  lgsdir2lem4  26356  lgsdir2lem5  26357  lgsne0  26363  1lgs  26368  gausslemma2dlem0e  26388  gausslemma2dlem0f  26389  gausslemma2dlem3  26396  gausslemma2d  26402  lgseisenlem1  26403  lgseisenlem2  26404  lgseisenlem3  26405  lgseisenlem4  26406  lgseisen  26407  lgsquadlem1  26408  lgsquadlem2  26409  lgsquad2lem1  26412  lgsquad2lem2  26413  m1lgs  26416  2lgslem3a  26424  2lgslem3b  26425  2lgslem3c  26426  2lgslem3d  26427  2lgsoddprmlem3a  26438  2lgsoddprmlem3b  26439  2lgsoddprmlem3c  26440  2lgsoddprmlem3d  26441  addsqnreup  26471  chebbnd1lem2  26498  chebbnd1lem3  26499  rplogsumlem2  26513  dchrisum0flblem1  26536  dchrisum0re  26541  mulog2sumlem2  26563  chpdifbndlem1  26581  pntpbnd1a  26613  pntpbnd2  26615  pntibndlem2  26619  pntibndlem3  26620  pntlemg  26626  pntlemk  26634  pntlemo  26635  axsegconlem1  27163  ax5seglem7  27181  axlowdimlem3  27190  axlowdimlem16  27203  axlowdimlem17  27204  elntg2  27231  vdegp1bi  27782  vtxdginducedm1  27788  wlkp1lem1  27918  spthispth  27970  2wlkdlem1  28166  2pthd  28181  clwlkclwwlkfo  28249  3wlkdlem1  28399  3pthd  28414  eucrct2eupth  28485  numclwwlk5  28628  numclwwlk7  28631  frgrregord013  28635  ex-fl  28687  ex-mod  28689  ex-exp  28690  ex-bc  28692  ex-lcm  28698  ex-ind-dvds  28701  vc2OLD  28806  vc0  28812  vcm  28814  nvm1  28903  nvpi  28905  nvmtri  28909  nvge0  28911  ipval3  28947  ipidsq  28948  ip0i  29063  ip1ilem  29064  ip2i  29066  ipdirilem  29067  ipasslem10  29077  siilem1  29089  siii  29091  minvecolem2  29113  hvsubid  29264  hvaddsubval  29271  hvmul2negi  29286  hvadd12i  29295  hv2times  29299  hvnegdii  29300  hvaddcani  29303  hi01  29334  hisubcomi  29342  normlem0  29347  normlem1  29348  normlem3  29350  normlem9  29356  bcseqi  29358  normsqi  29370  norm-ii-i  29375  normsubi  29379  norm3difi  29385  norm3adifii  29386  normpar2i  29394  polid2i  29395  polidi  29396  chdmm2i  29716  chj12i  29760  spanunsni  29817  qlaxr5i  29873  osumcor2i  29882  spansnji  29884  pjadjii  29912  pjinormii  29914  pjsslem  29917  pjpythi  29960  mayete3i  29966  mayetes3i  29967  hoadd12i  30015  honegneg  30044  ho2times  30057  hoaddsubi  30059  hosd1i  30060  hosd2i  30061  honpncani  30065  lnopeq0lem1  30243  lnopunilem1  30248  lnophmlem2  30255  lnfn0i  30280  nmopcoadji  30339  nmopcoadj2i  30340  opsqrlem1  30378  opsqrlem5  30382  opsqrlem6  30383  pjclem3  30435  stadd3i  30486  mddmd2  30547  mdexchi  30573  cvexchlem  30606  atomli  30620  atordi  30622  atabs2i  30640  mdsymlem1  30641  iuninc  30776  suppss2f  30850  suppss3  30936  dfdec100  31021  dpfrac1  31043  decdiv10  31047  dpmul100  31048  dp3mul10  31049  dpmul1000  31050  dpexpp1  31059  dpadd2  31061  dpadd  31062  dpmul  31064  dpmul4  31065  threehalves  31066  1mhdrd  31067  pfxlsw2ccat  31101  cyc2fv1  31265  cyc2fv2  31266  cycpmco2lem4  31273  cycpmco2lem5  31274  cyc3fv1  31281  cyc3fv2  31282  cyc3fv3  31283  archirngz  31320  gsumvsca2  31357  nn0omnd  31422  nn0archi  31424  xrge0slmod  31425  fedgmullem1  31587  fedgmullem2  31588  fedgmul  31589  lmatfvlem  31642  sqsscirc1  31735  cnvordtrestixx  31740  raddcn  31756  xrge0iifhom  31764  xrge0mulc1cn  31768  xrge0tmd  31772  lmlimxrge0  31775  qqhucn  31817  rrhcn  31822  qqtopn  31836  rrhqima  31839  brfae  32091  inelcarsg  32153  cndprobnul  32279  isrrvv  32285  ballotlem1  32328  ballotlem2  32330  ballotlemi1  32344  ballotlemii  32345  ballotlemic  32348  ballotlem1c  32349  ballotlemfrceq  32370  ballotth  32379  ofcs2  32399  signsvtn0  32424  signstfveq0  32431  signsvtp  32437  signsvtn  32438  signsvfpn  32439  signsvfnn  32440  signshf  32442  hashreprin  32475  reprfz1  32479  chtvalz  32484  breprexp  32488  breprexpnat  32489  hgt750lemd  32503  hgt750lem  32506  hgt750lem2  32507  subfacp1lem1  33016  subfacp1lem5  33021  subfacp1lem6  33022  subfaclim  33025  cvmliftlem5  33126  cvmliftlem8  33129  cvmliftlem10  33131  cvmliftlem13  33133  cvmlift2lem6  33145  cvmlift2lem12  33151  problem1  33498  problem2  33499  problem4  33501  quad3  33503  iexpire  33582  sin2h  35673  poimirlem16  35699  poimirlem17  35700  poimirlem18  35701  poimirlem19  35702  poimirlem20  35703  poimirlem21  35704  poimirlem22  35705  poimirlem26  35709  mblfinlem3  35722  ismblfin  35724  itg2addnclem3  35736  iblabsnc  35747  iblmulc2nc  35748  itgmulc2nc  35751  ftc1cnnc  35755  ftc1anclem6  35761  ftc1anclem7  35762  ftc1anclem8  35763  dvasin  35767  fdc  35809  heiborlem4  35878  heiborlem6  35880  dalem24  37617  pmod2iN  37769  cdleme9  38173  cdleme20aN  38229  cdleme22e  38264  cdleme22eALTN  38265  cdleme25cv  38278  cdleme29b  38295  cdlemh1  38735  cdlemh2  38736  cdlemk35  38832  cdlemkid1  38842  12gcd5e1  39918  60gcd7e1  39920  420gcd8e4  39921  12lcm5e60  39923  420lcm8e840  39926  lcm1un  39928  lcm2un  39929  lcm3un  39930  lcm4un  39931  lcm5un  39932  lcm6un  39933  lcm7un  39934  lcm8un  39935  3factsumint1  39936  3factsumint3  39938  lcmineqlem10  39953  3exp7  39968  3lexlogpow5ineq1  39969  3lexlogpow5ineq5  39975  aks4d1p1  39990  5bc2eq10  39998  2ap1caineq  40001  mhphf2  40181  sqmid3api  40204  sqn5i  40206  sqdeccom12  40210  235t711  40212  nn0expgcd  40228  re1m1e0m0  40273  readdid2  40279  remul02  40281  sn-1ticom  40309  sn-mulid2  40310  sn-0tie0  40314  sn-mul02  40315  sn-inelr  40328  flt4lem5e  40381  pellexlem5  40543  reglog1  40606  jm2.23  40706  jm2.27c  40717  lnmlsslnm  40794  lmhmlnmsplit  40800  areaquad  40935  resqrtvalex  41114  imsqrtvalex  41115  cotrclrcl  41212  inductionexd  41627  hashnzfz2  41801  lhe4.4ex1a  41809  binomcxplemdvsum  41835  binomcxplemnotnn0  41836  binomcxp  41837  sineq0ALT  42419  unirnmapsn  42616  fzisoeu  42702  fsummulc1f  42975  fprodexp  42998  constlimc  43028  sumnnodd  43034  limcresiooub  43046  limcresioolb  43047  cncfshiftioo  43296  fperdvper  43323  dvnmul  43347  dvmptfprod  43349  itgsinexplem1  43358  stoweidlem11  43415  stoweidlem13  43417  stoweidlem26  43430  stoweidlem34  43438  wallispilem4  43472  wallispi2lem1  43475  wallispi2lem2  43476  stirlinglem11  43488  dirkerper  43500  dirkertrigeqlem1  43502  dirkertrigeqlem3  43504  dirkercncflem1  43507  dirkercncflem4  43510  fourierdlem30  43541  fourierdlem32  43543  fourierdlem33  43544  fourierdlem42  43553  fourierdlem46  43556  fourierdlem47  43557  fourierdlem57  43567  fourierdlem60  43570  fourierdlem61  43571  fourierdlem62  43572  fourierdlem68  43578  fourierdlem73  43583  fourierdlem79  43589  fourierdlem89  43599  fourierdlem90  43600  fourierdlem91  43601  fourierdlem96  43606  fourierdlem97  43607  fourierdlem98  43608  fourierdlem99  43609  fourierdlem100  43610  fourierdlem103  43613  fourierdlem104  43614  fourierdlem108  43618  fourierdlem110  43620  fourierdlem113  43623  sqwvfoura  43632  sqwvfourb  43633  fourierswlem  43634  fouriersw  43635  fouriercn  43636  etransclem4  43642  etransclem7  43645  etransclem23  43661  etransclem24  43662  etransclem25  43663  etransclem26  43664  etransclem31  43669  etransclem32  43670  etransclem35  43673  etransclem37  43675  etransclem46  43684  rrndistlt  43694  sge0tsms  43781  sge0xaddlem2  43835  vonioolem2  44082  1t10e1p1e11  44663  deccarry  44664  1fzopredsuc  44677  m1mod0mod1  44682  iccpartgt  44740  fmtno0  44853  fmtno1  44854  fmtnorec2  44856  fmtno2  44863  fmtno3  44864  fmtno4  44865  fmtno5  44870  257prm  44874  fmtnofac1  44883  fmtno4prmfac  44885  fmtno4prmfac193  44886  fmtno4nprmfac193  44887  m2prm  44904  m3prm  44905  flsqrt5  44907  3ndvds4  44908  139prmALT  44909  31prm  44910  127prm  44912  m11nprm  44914  lighneallem2  44919  lighneallem3  44920  3exp4mod41  44929  41prothprmlem1  44930  41prothprmlem2  44931  41prothprm  44932  m1expevenALTV  44960  1oddALTV  45003  6even  45024  8even  45026  2exp340mod341  45046  341fppr2  45047  4fppr1  45048  8exp8mod9  45049  9fppr8  45050  nfermltl8rev  45055  gbpart7  45080  gbpart9  45082  gbpart11  45083  sbgoldbo  45100  bgoldbtbndlem1  45118  tgoldbachlt  45129  subsubmgm  45212  altgsumbcALT  45550  lincfsuppcl  45615  linccl  45616  lincvalsn  45619  lincdifsn  45626  lincsum  45631  lincscm  45632  lindslinindimp2lem4  45663  lindslinindsimp2lem5  45664  snlindsntor  45673  lincresunit3lem2  45682  zlmodzxzldeplem3  45704  ldepsnlinc  45710  nn0sumshdiglemA  45826  nn0sumshdiglemB  45827  ackval2  45889  ackval2012  45898  ackval3012  45899  ackval41a  45901  ackval42  45903  ackval42a  45904  affinecomb1  45909  rrx2linest  45949  itschlc0yqe  45967  itsclc0yqsollem1  45969  itscnhlc0xyqsol  45972  itschlc0xyqsol1  45973  itsclquadb  45983  2itscplem2  45986  itscnhlinecirc02plem2  45990  sinh-conventional  46300  onetansqsecsq  46322  cotsqcscsq  46323  mvlraddi  46333  mvrladdi  46334  mvlrmuli  46340  amgmwlem  46365  amgmlemALT  46366