Theorem oveq1i 7145

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

Syntax hints:   = wceq 1538  (class class class)co 7135

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-un 3886  df-in 3888  df-ss 3898  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4801  df-br 5031  df-iota 6283  df-fv 6332  df-ov 7138

This theorem is referenced by:  caov12  7356  caov411  7360  omopthlem1  8265  map1  8575  pw2eng  8606  fsuppunbi  8838  cnfcomlem  9146  cnfcom2  9149  infxpenc2  9433  adderpqlem  10365  addassnq  10369  distrnq  10372  halfnq  10387  archnq  10391  addclprlem2  10428  addcmpblnr  10480  ltsrpr  10488  m1m1sr  10504  recexsrlem  10514  sqgt0sr  10517  map2psrpr  10521  axi2m1  10570  axcnre  10575  mul02lem2  10806  addid1  10809  cnegex2  10811  addid2  10812  mvrraddi  10892  mvlladdi  10893  negsubdi  10931  mulneg1  11065  recextlem1  11259  recdiv  11335  divmul13i  11390  mvllmuli  11462  2p2e4  11760  2times  11761  1p2e3  11768  3p2e5  11776  3p3e6  11777  4p2e6  11778  4p3e7  11779  4p4e8  11780  5p2e7  11781  5p3e8  11782  5p4e9  11783  6p2e8  11784  6p3e9  11785  7p2e9  11786  1mhlfehlf  11844  8th4div3  11845  halfpm6th  11846  nneo  12054  9p1e10  12088  dfdec10  12089  num0h  12098  numsuc  12100  dec10p  12129  numma  12130  nummac  12131  numma2c  12132  numadd  12133  numaddc  12134  nummul2c  12136  decaddci  12147  decsubi  12149  5p5e10  12157  6p4e10  12158  7p3e10  12161  8p2e10  12166  decbin0  12226  decbin2  12227  xmulm1  12662  xadddi2  12678  x2times  12680  elfzp1b  12979  elfzm1b  12980  fz1ssfz0  12998  fz0to4untppr  13005  fz0sn0fz1  13019  fz0add1fz1  13102  elfz0lmr  13147  fldiv4p1lem1div2  13200  quoremz  13218  quoremnn0ALT  13220  uzrdgxfr  13330  mulexpz  13465  expaddz  13469  sqrecii  13542  sq4e2t8  13558  cu2  13559  i3  13562  iexpcyc  13565  binom2i  13570  binom3  13581  crreczi  13585  discr  13597  3dec  13622  nn0opthlem1  13624  nn0opth2i  13627  faclbnd  13646  bcp1nk  13673  bcpasc  13677  hashp1i  13760  hashxplem  13790  hashpw  13793  hashfun  13794  hashbc  13807  ccatlid  13931  pfxccatin12lem2c  14083  revs1  14118  cats1cat  14214  cats2cat  14215  lsws2  14257  lsws3  14258  lsws4  14259  s3s4  14286  s2s5  14287  s5s2  14288  imre  14459  crim  14466  remullem  14479  cnpart  14591  sqrtneglem  14618  absexpz  14657  absimle  14661  sqreulem  14711  amgm2  14721  iseraltlem2  15031  iseraltlem3  15032  modfsummod  15141  binomlem  15176  binom11  15179  arisum  15207  arisum2  15208  pwdif  15215  georeclim  15220  geo2sum  15221  mertenslem1  15232  mertens  15234  prodfrec  15243  fprodm1s  15316  fprodp1s  15317  fprodmodd  15343  fallfacfwd  15382  0risefac  15384  bpolydiflem  15400  bpoly2  15403  bpoly3  15404  bpoly4  15405  fsumcube  15406  efzval  15447  resinval  15480  recosval  15481  efi4p  15482  tan0  15496  efival  15497  sinhval  15499  coshval  15500  cosadd  15510  cos2tsin  15524  ef01bndlem  15529  cos1bnd  15532  cos2bnd  15533  absefib  15543  efieq1re  15544  demoivreALT  15546  eirrlem  15549  rpnnen2lem3  15561  rpnnen2lem11  15569  ruclem7  15581  3dvds  15672  3dvdsdec  15673  3dvds2dec  15674  odd2np1  15682  nn0o1gt2  15722  nn0o  15724  pwp1fsum  15732  divalglem2  15736  divalglem9  15742  flodddiv4  15754  m1bits  15779  sadcp1  15794  sadeq  15811  smupp1  15819  smumul  15832  gcdaddmlem  15862  3lcm2e6woprm  15949  nn0gcdsq  16082  phiprmpw  16103  prmdiv  16112  prmdiveq  16113  pythagtriplem1  16143  pythagtriplem12  16153  pythagtriplem14  16155  pockthi  16233  infpnlem1  16236  prmreclem4  16245  4sqlem12  16282  4sqlem13  16283  4sqlem19  16289  vdwapun  16300  vdwlem6  16312  0hashbc  16333  prmo2  16366  prmo3  16367  dec5dvds  16390  dec5nprm  16392  dec2nprm  16393  modxai  16394  modxp1i  16396  mod2xnegi  16397  modsubi  16398  gcdmodi  16400  decexp2  16401  decsplit0b  16406  decsplit1  16408  decsplit  16409  karatsuba  16410  2exp7  16414  2exp8  16415  3exp3  16417  5prm  16434  7prm  16436  11prm  16440  prmlem2  16445  37prm  16446  43prm  16447  83prm  16448  139prm  16449  163prm  16450  317prm  16451  631prm  16452  prmo5  16454  1259lem1  16456  1259lem2  16457  1259lem3  16458  1259lem4  16459  1259lem5  16460  2503lem1  16462  2503lem2  16463  2503lem3  16464  2503prm  16465  4001lem1  16466  4001lem2  16467  4001lem3  16468  4001lem4  16469  4001prm  16470  pwsbas  16752  rcaninv  17056  subsubc  17115  xpccatid  17430  subsubm  17973  smndex2dnrinv  18072  mulg2  18229  subsubg  18294  oppgmnd  18474  gsumwrev  18486  psgnunilem2  18615  sylow1lem1  18715  subgslw  18733  sylow3  18750  efginvrel2  18845  efgsfo  18857  frgpnabllem1  18986  gsumzaddlem  19034  gsummptfzsplitl  19046  gsummpt1n0  19078  dprdfid  19132  ablfac1lem  19183  pgpfac1lem3  19192  pgpfaclem1  19196  ablsimpgfindlem1  19222  mgpress  19243  srgbinomlem4  19286  opprring  19377  unitsubm  19416  subsubrg  19554  cntzsdrg  19574  subdrgint  19575  lsslss  19726  xrsnsgrp  20127  gzrngunit  20157  expghm  20189  chrid  20219  zrhpsgnmhm  20273  psgndiflemA  20290  frlmip  20467  frlmphl  20470  evlsval  20758  mpff  20776  coe1fzgsumdlem  20930  evl1gsumdlem  20980  matvsca2  21033  mattposvs  21060  m2detleiblem3  21234  m2detleiblem4  21235  cpmidpmat  21478  resstopn  21791  cnmpt1res  22281  ressuss  22869  iscusp2  22908  ucnextcn  22910  txmetcnp  23154  rerest  23409  xrtgioo  23411  xrrest  23412  cnmpopc  23533  xrhmeo  23551  clmvs2  23699  clmnegneg  23709  ncvsm1  23759  ncvspi  23761  cphassir  23820  cphipval2  23845  reust  23985  rrxprds  23993  csbren  24003  rrxdsfi  24015  minveclem2  24030  ovolunlem1a  24100  ovolicc2lem4  24124  uniioombllem5  24191  iblabs  24432  iblabsr  24433  iblmulc2  24434  itgmulc2  24437  limcres  24489  dvfval  24500  dvreslem  24512  dvres2lem  24513  dvcnp2  24523  cpnres  24540  dvcobr  24549  dveflem  24582  lhop1lem  24616  lhop2  24618  dvcnvrelem2  24621  plyun0  24794  coeeulem  24821  coeeu  24822  dvply1  24880  dvtaylp  24965  taylthlem2  24969  taylth  24970  dvradcnv  25016  pserdvlem2  25023  abelthlem8  25034  abelth  25036  sinhalfpilem  25056  cospi  25065  eulerid  25067  cos2pi  25069  ef2kpi  25071  sinhalfpip  25085  sinhalfpim  25086  coshalfpip  25087  coshalfpim  25088  sincosq3sgn  25093  sincosq4sgn  25094  tangtx  25098  sincos4thpi  25106  sincos6thpi  25108  sineq0  25116  tanregt0  25131  logm1  25180  abslogle  25209  tanarg  25210  logcnlem4  25236  advlogexp  25246  cxpsqrt  25294  dvsqrt  25331  dvcnsqrt  25333  cxpcn3  25337  root1cj  25345  cxpeq  25346  logb1  25355  2logb9irr  25381  sqrt2cxp2logb9e3  25385  ang180lem1  25395  ang180lem2  25396  ang180lem3  25397  lawcos  25402  isosctrlem1  25404  isosctrlem2  25405  quad2  25425  1cubrlem  25427  1cubr  25428  dcubic2  25430  mcubic  25433  binom4  25436  dquartlem1  25437  quart1lem  25441  quart1  25442  quartlem1  25443  asinlem  25454  asinlem2  25455  asinlem3a  25456  acosneg  25473  efiasin  25474  asinsinlem  25477  asinsin  25478  acoscos  25479  asin1  25480  acosbnd  25486  atancj  25496  efiatan  25498  atanlogaddlem  25499  efiatan2  25503  2efiatan  25504  tanatan  25505  cosatan  25507  atantan  25509  atanbndlem  25511  atans2  25517  dvatan  25521  atantayl  25523  atantayl2  25524  log2cnv  25530  log2tlbnd  25531  log2ublem2  25533  log2ublem3  25534  log2ub  25535  birthday  25540  jensenlem1  25572  amgmlem  25575  lgamgulmlem2  25615  lgamgulmlem5  25618  lgambdd  25622  ftalem2  25659  ftalem5  25662  ftalem6  25663  basellem2  25667  basellem3  25668  basellem5  25670  basellem8  25673  basellem9  25674  mule1  25733  ppi1i  25753  musum  25776  ppiublem1  25786  ppiub  25788  chtublem  25795  chtub  25796  dchrptlem1  25848  dchrptlem2  25849  bclbnd  25864  bposlem6  25873  bposlem8  25875  bposlem9  25876  lgsdir2lem1  25909  lgsdir2lem2  25910  lgsdir2lem4  25912  lgsdir2lem5  25913  lgsne0  25919  1lgs  25924  gausslemma2dlem0e  25944  gausslemma2dlem0f  25945  gausslemma2dlem3  25952  gausslemma2d  25958  lgseisenlem1  25959  lgseisenlem2  25960  lgseisenlem3  25961  lgseisenlem4  25962  lgseisen  25963  lgsquadlem1  25964  lgsquadlem2  25965  lgsquad2lem1  25968  lgsquad2lem2  25969  m1lgs  25972  2lgslem3a  25980  2lgslem3b  25981  2lgslem3c  25982  2lgslem3d  25983  2lgsoddprmlem3a  25994  2lgsoddprmlem3b  25995  2lgsoddprmlem3c  25996  2lgsoddprmlem3d  25997  addsqnreup  26027  chebbnd1lem2  26054  chebbnd1lem3  26055  rplogsumlem2  26069  dchrisum0flblem1  26092  dchrisum0re  26097  mulog2sumlem2  26119  chpdifbndlem1  26137  pntpbnd1a  26169  pntpbnd2  26171  pntibndlem2  26175  pntibndlem3  26176  pntlemg  26182  pntlemk  26190  pntlemo  26191  axsegconlem1  26711  ax5seglem7  26729  axlowdimlem3  26738  axlowdimlem16  26751  axlowdimlem17  26752  elntg2  26779  vdegp1bi  27327  vtxdginducedm1  27333  wlkp1lem1  27463  spthispth  27515  2wlkdlem1  27711  2pthd  27726  clwlkclwwlkfo  27794  3wlkdlem1  27944  3pthd  27959  eucrct2eupth  28030  numclwwlk5  28173  numclwwlk7  28176  frgrregord013  28180  ex-fl  28232  ex-mod  28234  ex-exp  28235  ex-bc  28237  ex-lcm  28243  ex-ind-dvds  28246  vc2OLD  28351  vc0  28357  vcm  28359  nvm1  28448  nvpi  28450  nvmtri  28454  nvge0  28456  ipval3  28492  ipidsq  28493  ip0i  28608  ip1ilem  28609  ip2i  28611  ipdirilem  28612  ipasslem10  28622  siilem1  28634  siii  28636  minvecolem2  28658  hvsubid  28809  hvaddsubval  28816  hvmul2negi  28831  hvadd12i  28840  hv2times  28844  hvnegdii  28845  hvaddcani  28848  hi01  28879  hisubcomi  28887  normlem0  28892  normlem1  28893  normlem3  28895  normlem9  28901  bcseqi  28903  normsqi  28915  norm-ii-i  28920  normsubi  28924  norm3difi  28930  norm3adifii  28931  normpar2i  28939  polid2i  28940  polidi  28941  chdmm2i  29261  chj12i  29305  spanunsni  29362  qlaxr5i  29418  osumcor2i  29427  spansnji  29429  pjadjii  29457  pjinormii  29459  pjsslem  29462  pjpythi  29505  mayete3i  29511  mayetes3i  29512  hoadd12i  29560  honegneg  29589  ho2times  29602  hoaddsubi  29604  hosd1i  29605  hosd2i  29606  honpncani  29610  lnopeq0lem1  29788  lnopunilem1  29793  lnophmlem2  29800  lnfn0i  29825  nmopcoadji  29884  nmopcoadj2i  29885  opsqrlem1  29923  opsqrlem5  29927  opsqrlem6  29928  pjclem3  29980  stadd3i  30031  mddmd2  30092  mdexchi  30118  cvexchlem  30151  atomli  30165  atordi  30167  atabs2i  30185  mdsymlem1  30186  iuninc  30324  suppss2f  30398  suppss3  30486  dfdec100  30572  dpfrac1  30594  decdiv10  30598  dpmul100  30599  dp3mul10  30600  dpmul1000  30601  dpexpp1  30610  dpadd2  30612  dpadd  30613  dpmul  30615  dpmul4  30616  threehalves  30617  1mhdrd  30618  pfxlsw2ccat  30652  cyc2fv1  30813  cyc2fv2  30814  cycpmco2lem4  30821  cycpmco2lem5  30822  cyc3fv1  30829  cyc3fv2  30830  cyc3fv3  30831  archirngz  30868  gsumvsca2  30905  nn0omnd  30965  nn0archi  30967  xrge0slmod  30968  fedgmullem1  31113  fedgmullem2  31114  fedgmul  31115  lmatfvlem  31168  sqsscirc1  31261  cnvordtrestixx  31266  raddcn  31282  xrge0iifhom  31290  xrge0mulc1cn  31294  xrge0tmd  31298  lmlimxrge0  31301  qqhucn  31343  rrhcn  31348  qqtopn  31362  rrhqima  31365  brfae  31617  inelcarsg  31679  cndprobnul  31805  isrrvv  31811  ballotlem1  31854  ballotlem2  31856  ballotlemi1  31870  ballotlemii  31871  ballotlemic  31874  ballotlem1c  31875  ballotlemfrceq  31896  ballotth  31905  ofcs2  31925  signsvtn0  31950  signstfveq0  31957  signsvtp  31963  signsvtn  31964  signsvfpn  31965  signsvfnn  31966  signshf  31968  hashreprin  32001  reprfz1  32005  chtvalz  32010  breprexp  32014  breprexpnat  32015  hgt750lemd  32029  hgt750lem  32032  hgt750lem2  32033  subfacp1lem1  32539  subfacp1lem5  32544  subfacp1lem6  32545  subfaclim  32548  cvmliftlem5  32649  cvmliftlem8  32652  cvmliftlem10  32654  cvmliftlem13  32656  cvmlift2lem6  32668  cvmlift2lem12  32674  problem1  33021  problem2  33022  problem4  33024  quad3  33026  iexpire  33080  sin2h  35047  poimirlem16  35073  poimirlem17  35074  poimirlem18  35075  poimirlem19  35076  poimirlem20  35077  poimirlem21  35078  poimirlem22  35079  poimirlem26  35083  mblfinlem3  35096  ismblfin  35098  itg2addnclem3  35110  iblabsnc  35121  iblmulc2nc  35122  itgmulc2nc  35125  ftc1cnnc  35129  ftc1anclem6  35135  ftc1anclem7  35136  ftc1anclem8  35137  dvasin  35141  fdc  35183  heiborlem4  35252  heiborlem6  35254  dalem24  36993  pmod2iN  37145  cdleme9  37549  cdleme20aN  37605  cdleme22e  37640  cdleme22eALTN  37641  cdleme25cv  37654  cdleme29b  37671  cdlemh1  38111  cdlemh2  38112  cdlemk35  38208  cdlemkid1  38218  12gcd5e1  39291  60gcd7e1  39293  420gcd8e4  39294  12lcm5e60  39296  420lcm8e840  39299  lcm1un  39301  lcm2un  39302  lcm3un  39303  lcm4un  39304  lcm5un  39305  lcm6un  39306  lcm7un  39307  lcm8un  39308  3factsumint1  39309  3factsumint3  39311  lcmineqlem10  39326  3lexlogpow5ineq1  39341  5bc2eq10  39346  2ap1caineq  39349  sqmid3api  39477  sqn5i  39479  sqdeccom12  39483  235t711  39485  nn0expgcd  39492  re1m1e0m0  39535  readdid2  39541  remul02  39543  sn-1ticom  39571  sn-mulid2  39572  sn-0tie0  39576  sn-mul02  39577  sn-inelr  39590  pellexlem5  39774  reglog1  39837  jm2.23  39937  jm2.27c  39948  lnmlsslnm  40025  lmhmlnmsplit  40031  areaquad  40166  resqrtvalex  40345  imsqrtvalex  40346  cotrclrcl  40443  inductionexd  40858  hashnzfz2  41025  lhe4.4ex1a  41033  binomcxplemdvsum  41059  binomcxplemnotnn0  41060  binomcxp  41061  sineq0ALT  41643  unirnmapsn  41843  fzisoeu  41932  fsummulc1f  42212  fprodexp  42236  constlimc  42266  sumnnodd  42272  limcresiooub  42284  limcresioolb  42285  cncfshiftioo  42534  fperdvper  42561  dvnmul  42585  dvmptfprod  42587  itgsinexplem1  42596  stoweidlem11  42653  stoweidlem13  42655  stoweidlem26  42668  stoweidlem34  42676  wallispilem4  42710  wallispi2lem1  42713  wallispi2lem2  42714  stirlinglem11  42726  dirkerper  42738  dirkertrigeqlem1  42740  dirkertrigeqlem3  42742  dirkercncflem1  42745  dirkercncflem4  42748  fourierdlem30  42779  fourierdlem32  42781  fourierdlem33  42782  fourierdlem42  42791  fourierdlem46  42794  fourierdlem47  42795  fourierdlem57  42805  fourierdlem60  42808  fourierdlem61  42809  fourierdlem62  42810  fourierdlem68  42816  fourierdlem73  42821  fourierdlem79  42827  fourierdlem89  42837  fourierdlem90  42838  fourierdlem91  42839  fourierdlem96  42844  fourierdlem97  42845  fourierdlem98  42846  fourierdlem99  42847  fourierdlem100  42848  fourierdlem103  42851  fourierdlem104  42852  fourierdlem108  42856  fourierdlem110  42858  fourierdlem113  42861  sqwvfoura  42870  sqwvfourb  42871  fourierswlem  42872  fouriersw  42873  fouriercn  42874  etransclem4  42880  etransclem7  42883  etransclem23  42899  etransclem24  42900  etransclem25  42901  etransclem26  42902  etransclem31  42907  etransclem32  42908  etransclem35  42911  etransclem37  42913  etransclem46  42922  rrndistlt  42932  sge0tsms  43019  sge0xaddlem2  43073  vonioolem2  43320  1t10e1p1e11  43867  deccarry  43868  1fzopredsuc  43881  m1mod0mod1  43886  iccpartgt  43944  fmtno0  44057  fmtno1  44058  fmtnorec2  44060  fmtno2  44067  fmtno3  44068  fmtno4  44069  fmtno5  44074  257prm  44078  fmtnofac1  44087  fmtno4prmfac  44089  fmtno4prmfac193  44090  fmtno4nprmfac193  44091  m2prm  44108  m3prm  44109  flsqrt5  44111  3ndvds4  44112  139prmALT  44113  31prm  44114  127prm  44116  m11nprm  44119  lighneallem2  44124  lighneallem3  44125  3exp4mod41  44134  41prothprmlem1  44135  41prothprmlem2  44136  41prothprm  44137  m1expevenALTV  44165  1oddALTV  44208  6even  44229  8even  44231  2exp340mod341  44251  341fppr2  44252  4fppr1  44253  8exp8mod9  44254  9fppr8  44255  nfermltl8rev  44260  gbpart7  44285  gbpart9  44287  gbpart11  44288  sbgoldbo  44305  bgoldbtbndlem1  44323  tgoldbachlt  44334  subsubmgm  44417  altgsumbcALT  44755  lincfsuppcl  44822  linccl  44823  lincvalsn  44826  lincdifsn  44833  lincsum  44838  lincscm  44839  lindslinindimp2lem4  44870  lindslinindsimp2lem5  44871  snlindsntor  44880  lincresunit3lem2  44889  zlmodzxzldeplem3  44911  ldepsnlinc  44917  nn0sumshdiglemA  45033  nn0sumshdiglemB  45034  ackval2  45096  ackval2012  45105  ackval3012  45106  ackval41a  45108  ackval42  45110  ackval42a  45111  affinecomb1  45116  rrx2linest  45156  itschlc0yqe  45174  itsclc0yqsollem1  45176  itscnhlc0xyqsol  45179  itschlc0xyqsol1  45180  itsclquadb  45190  2itscplem2  45193  itscnhlinecirc02plem2  45197  sinh-conventional  45265  onetansqsecsq  45287  cotsqcscsq  45288  mvlraddi  45298  mvrladdi  45299  mvlrmuli  45305  amgmwlem  45330  amgmlemALT  45331