Theorem oveq1i 7422

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

Syntax hints:   = wceq 1540  (class class class)co 7412

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2723  df-clel 2809  df-rab 3432  df-v 3475  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-iota 6495  df-fv 6551  df-ov 7415

This theorem is referenced by:  caov12  7639  caov411  7643  omopthlem1  8664  map1  9046  pw2eng  9084  fsuppunbi  9390  cnfcomlem  9700  cnfcom2  9703  infxpenc2  10023  adderpqlem  10955  addassnq  10959  distrnq  10962  halfnq  10977  archnq  10981  addclprlem2  11018  addcmpblnr  11070  ltsrpr  11078  m1m1sr  11094  recexsrlem  11104  sqgt0sr  11107  map2psrpr  11111  axi2m1  11160  axcnre  11165  mul02lem2  11398  addrid  11401  cnegex2  11403  addlid  11404  mvrraddi  11484  mvlladdi  11485  negsubdi  11523  mulneg1  11657  recextlem1  11851  recdiv  11927  divmul13i  11982  mvllmuli  12054  2p2e4  12354  2times  12355  1p2e3  12362  3p2e5  12370  3p3e6  12371  4p2e6  12372  4p3e7  12373  4p4e8  12374  5p2e7  12375  5p3e8  12376  5p4e9  12377  6p2e8  12378  6p3e9  12379  7p2e9  12380  1mhlfehlf  12438  8th4div3  12439  halfpm6th  12440  nneo  12653  9p1e10  12686  dfdec10  12687  num0h  12696  numsuc  12698  dec10p  12727  numma  12728  nummac  12729  numma2c  12730  numadd  12731  numaddc  12732  nummul2c  12734  decaddci  12745  decsubi  12747  5p5e10  12755  6p4e10  12756  7p3e10  12759  8p2e10  12764  decbin0  12824  decbin2  12825  xmulm1  13267  xadddi2  13283  x2times  13285  elfzp1b  13585  elfzm1b  13586  fz1ssfz0  13604  fz0to4untppr  13611  fz0sn0fz1  13625  fz0add1fz1  13709  elfz0lmr  13754  fldiv4p1lem1div2  13807  quoremz  13827  quoremnn0ALT  13829  uzrdgxfr  13939  mulexpz  14075  expaddz  14079  sqrecii  14154  sq4e2t8  14170  cu2  14171  i3  14174  iexpcyc  14178  binom2i  14183  binom3  14194  crreczi  14198  discr  14210  3dec  14233  nn0opthlem1  14235  nn0opth2i  14238  faclbnd  14257  bcp1nk  14284  bcpasc  14288  hashp1i  14370  hashxplem  14400  hashpw  14403  hashfun  14404  hashbc  14419  ccatlid  14543  pfxccatin12lem2c  14687  revs1  14722  cats1cat  14819  cats2cat  14820  lsws2  14862  lsws3  14863  lsws4  14864  s3s4  14891  s2s5  14892  s5s2  14893  imre  15062  crim  15069  remullem  15082  cnpart  15194  sqrtneglem  15220  absexpz  15259  absimle  15263  sqreulem  15313  amgm2  15323  iseraltlem2  15636  iseraltlem3  15637  modfsummod  15747  binomlem  15782  binom11  15785  arisum  15813  arisum2  15814  pwdif  15821  georeclim  15825  geo2sum  15826  mertenslem1  15837  mertens  15839  prodfrec  15848  fprodm1s  15921  fprodp1s  15922  fprodmodd  15948  fallfacfwd  15987  0risefac  15989  bpolydiflem  16005  bpoly2  16008  bpoly3  16009  bpoly4  16010  fsumcube  16011  efzval  16052  resinval  16085  recosval  16086  efi4p  16087  tan0  16101  efival  16102  sinhval  16104  coshval  16105  cosadd  16115  cos2tsin  16129  ef01bndlem  16134  cos1bnd  16137  cos2bnd  16138  absefib  16148  efieq1re  16149  demoivreALT  16151  eirrlem  16154  rpnnen2lem3  16166  rpnnen2lem11  16174  ruclem7  16186  3dvds  16281  3dvdsdec  16282  3dvds2dec  16283  odd2np1  16291  nn0o1gt2  16331  nn0o  16333  pwp1fsum  16341  divalglem2  16345  divalglem9  16351  flodddiv4  16363  m1bits  16388  sadcp1  16403  sadeq  16420  smupp1  16428  smumul  16441  gcdaddmlem  16472  3lcm2e6woprm  16559  nn0gcdsq  16695  phiprmpw  16716  prmdiv  16725  prmdiveq  16726  pythagtriplem1  16756  pythagtriplem12  16766  pythagtriplem14  16768  pockthi  16847  infpnlem1  16850  prmreclem4  16859  4sqlem12  16896  4sqlem13  16897  4sqlem19  16903  vdwapun  16914  vdwlem6  16926  0hashbc  16947  prmo2  16980  prmo3  16981  dec5dvds  17004  dec5nprm  17006  dec2nprm  17007  modxai  17008  modxp1i  17010  mod2xnegi  17011  modsubi  17012  gcdmodi  17014  decexp2  17015  decsplit0b  17020  decsplit1  17022  decsplit  17023  karatsuba  17024  2exp7  17028  2exp8  17029  3exp3  17032  5prm  17049  7prm  17051  11prm  17055  prmlem2  17060  37prm  17061  43prm  17062  83prm  17063  139prm  17064  163prm  17065  317prm  17066  631prm  17067  prmo5  17069  1259lem1  17071  1259lem2  17072  1259lem3  17073  1259lem4  17074  1259lem5  17075  2503lem1  17077  2503lem2  17078  2503lem3  17079  2503prm  17080  4001lem1  17081  4001lem2  17082  4001lem3  17083  4001lem4  17084  4001prm  17085  pwsbas  17440  rcaninv  17748  subsubc  17810  xpccatid  18150  subsubmgm  18641  subsubm  18739  smndex2dnrinv  18838  mulg2  19006  subsubg  19072  oppgmnd  19269  gsumwrev  19281  psgnunilem2  19411  sylow1lem1  19514  subgslw  19532  sylow3  19549  efginvrel2  19643  efgsfo  19655  frgpnabllem1  19789  gsumzaddlem  19837  gsummptfzsplitl  19849  gsummpt1n0  19881  dprdfid  19935  ablfac1lem  19986  pgpfac1lem3  19995  pgpfaclem1  19999  ablsimpgfindlem1  20025  mgpress  20050  mgpressOLD  20051  srgbinomlem4  20130  opprrng  20243  unitsubm  20284  subsubrng  20459  subsubrg  20496  cntzsdrg  20649  subdrgint  20650  lsslss  20804  xrsnsgrp  21270  gzrngunit  21300  expghm  21335  pzriprng1ALT  21356  chrid  21389  zrhpsgnmhm  21447  psgndiflemA  21464  frlmip  21643  frlmphl  21646  evlsval  21960  mpff  21978  coe1fzgsumdlem  22145  evl1gsumdlem  22195  matvsca2  22250  mattposvs  22277  m2detleiblem3  22451  m2detleiblem4  22452  cpmidpmat  22695  resstopn  23010  cnmpt1res  23500  ressuss  24087  iscusp2  24127  ucnextcn  24129  txmetcnp  24376  rerest  24640  xrtgioo  24642  xrrest  24643  cnmpopc  24769  xrhmeo  24791  clmvs2  24941  clmnegneg  24951  ncvsm1  25002  ncvspi  25004  cphassir  25063  cphipval2  25089  reust  25229  rrxprds  25237  csbren  25247  rrxdsfi  25259  minveclem2  25274  ovolunlem1a  25345  ovolicc2lem4  25369  uniioombllem5  25436  iblabs  25678  iblabsr  25679  iblmulc2  25680  itgmulc2  25683  limcres  25735  dvfval  25746  dvreslem  25758  dvres2lem  25759  dvcnp2  25769  dvcnp2OLD  25770  cpnres  25787  dvmulbr  25789  dvcobr  25797  dvcobrOLD  25798  dveflem  25831  lhop1lem  25866  lhop2  25868  dvcnvrelem2  25871  plyun0  26049  coeeulem  26076  coeeu  26077  dvply1  26136  dvtaylp  26221  taylthlem2  26225  taylth  26226  dvradcnv  26272  pserdvlem2  26280  abelthlem8  26291  abelth  26293  sinhalfpilem  26313  cospi  26322  eulerid  26324  cos2pi  26326  ef2kpi  26328  sinhalfpip  26342  sinhalfpim  26343  coshalfpip  26344  coshalfpim  26345  sincosq3sgn  26350  sincosq4sgn  26351  tangtx  26355  sincos4thpi  26363  sincos6thpi  26365  sineq0  26373  tanregt0  26388  logm1  26437  abslogle  26466  tanarg  26467  logcnlem4  26493  advlogexp  26503  cxpsqrt  26551  dvsqrt  26590  dvcnsqrt  26592  cxpcn3  26597  root1cj  26605  cxpeq  26606  logb1  26615  2logb9irr  26641  sqrt2cxp2logb9e3  26645  ang180lem1  26655  ang180lem2  26656  ang180lem3  26657  lawcos  26662  isosctrlem1  26664  isosctrlem2  26665  quad2  26685  1cubrlem  26687  1cubr  26688  dcubic2  26690  mcubic  26693  binom4  26696  dquartlem1  26697  quart1lem  26701  quart1  26702  quartlem1  26703  asinlem  26714  asinlem2  26715  asinlem3a  26716  acosneg  26733  efiasin  26734  asinsinlem  26737  asinsin  26738  acoscos  26739  asin1  26740  acosbnd  26746  atancj  26756  efiatan  26758  atanlogaddlem  26759  efiatan2  26763  2efiatan  26764  tanatan  26765  cosatan  26767  atantan  26769  atanbndlem  26771  atans2  26777  dvatan  26781  atantayl  26783  atantayl2  26784  log2cnv  26790  log2tlbnd  26791  log2ublem2  26793  log2ublem3  26794  log2ub  26795  birthday  26800  jensenlem1  26832  amgmlem  26835  lgamgulmlem2  26875  lgamgulmlem5  26878  lgambdd  26882  ftalem2  26919  ftalem5  26922  ftalem6  26923  basellem2  26927  basellem3  26928  basellem5  26930  basellem8  26933  basellem9  26934  mule1  26993  ppi1i  27013  musum  27036  ppiublem1  27048  ppiub  27050  chtublem  27057  chtub  27058  dchrptlem1  27110  dchrptlem2  27111  bclbnd  27126  bposlem6  27135  bposlem8  27137  bposlem9  27138  lgsdir2lem1  27171  lgsdir2lem2  27172  lgsdir2lem4  27174  lgsdir2lem5  27175  lgsne0  27181  1lgs  27186  gausslemma2dlem0e  27206  gausslemma2dlem0f  27207  gausslemma2dlem3  27214  gausslemma2d  27220  lgseisenlem1  27221  lgseisenlem2  27222  lgseisenlem3  27223  lgseisenlem4  27224  lgseisen  27225  lgsquadlem1  27226  lgsquadlem2  27227  lgsquad2lem1  27230  lgsquad2lem2  27231  m1lgs  27234  2lgslem3a  27242  2lgslem3b  27243  2lgslem3c  27244  2lgslem3d  27245  2lgsoddprmlem3a  27256  2lgsoddprmlem3b  27257  2lgsoddprmlem3c  27258  2lgsoddprmlem3d  27259  addsqnreup  27289  chebbnd1lem2  27316  chebbnd1lem3  27317  rplogsumlem2  27331  dchrisum0flblem1  27354  dchrisum0re  27359  mulog2sumlem2  27381  chpdifbndlem1  27399  pntpbnd1a  27431  pntpbnd2  27433  pntibndlem2  27437  pntibndlem3  27438  pntlemg  27444  pntlemk  27452  pntlemo  27453  remulscllem1  28108  axsegconlem1  28608  ax5seglem7  28626  axlowdimlem3  28635  axlowdimlem16  28648  axlowdimlem17  28649  elntg2  28676  vdegp1bi  29227  vtxdginducedm1  29233  wlkp1lem1  29363  spthispth  29416  2wlkdlem1  29612  2pthd  29627  clwlkclwwlkfo  29695  3wlkdlem1  29845  3pthd  29860  eucrct2eupth  29931  numclwwlk5  30074  numclwwlk7  30077  frgrregord013  30081  ex-fl  30133  ex-mod  30135  ex-exp  30136  ex-bc  30138  ex-lcm  30144  ex-ind-dvds  30147  vc2OLD  30254  vc0  30260  vcm  30262  nvm1  30351  nvpi  30353  nvmtri  30357  nvge0  30359  ipval3  30395  ipidsq  30396  ip0i  30511  ip1ilem  30512  ip2i  30514  ipdirilem  30515  ipasslem10  30525  siilem1  30537  siii  30539  minvecolem2  30561  hvsubid  30712  hvaddsubval  30719  hvmul2negi  30734  hvadd12i  30743  hv2times  30747  hvnegdii  30748  hvaddcani  30751  hi01  30782  hisubcomi  30790  normlem0  30795  normlem1  30796  normlem3  30798  normlem9  30804  bcseqi  30806  normsqi  30818  norm-ii-i  30823  normsubi  30827  norm3difi  30833  norm3adifii  30834  normpar2i  30842  polid2i  30843  polidi  30844  chdmm2i  31164  chj12i  31208  spanunsni  31265  qlaxr5i  31321  osumcor2i  31330  spansnji  31332  pjadjii  31360  pjinormii  31362  pjsslem  31365  pjpythi  31408  mayete3i  31414  mayetes3i  31415  hoadd12i  31463  honegneg  31492  ho2times  31505  hoaddsubi  31507  hosd1i  31508  hosd2i  31509  honpncani  31513  lnopeq0lem1  31691  lnopunilem1  31696  lnophmlem2  31703  lnfn0i  31728  nmopcoadji  31787  nmopcoadj2i  31788  opsqrlem1  31826  opsqrlem5  31830  opsqrlem6  31831  pjclem3  31883  stadd3i  31934  mddmd2  31995  mdexchi  32021  cvexchlem  32054  atomli  32068  atordi  32070  atabs2i  32088  mdsymlem1  32089  iuninc  32225  suppss2f  32296  mptiffisupp  32348  suppss3  32382  dfdec100  32469  dpfrac1  32491  decdiv10  32495  dpmul100  32496  dp3mul10  32497  dpmul1000  32498  dpexpp1  32507  dpadd2  32509  dpadd  32510  dpmul  32512  dpmul4  32513  threehalves  32514  1mhdrd  32515  pfxlsw2ccat  32549  cyc2fv1  32716  cyc2fv2  32717  cycpmco2lem4  32724  cycpmco2lem5  32725  cyc3fv1  32732  cyc3fv2  32733  cyc3fv3  32734  archirngz  32771  gsumvsca2  32808  nn0omnd  32896  nn0archi  32898  xrge0slmod  32899  opprabs  33036  resssra  33128  lsssra  33129  fedgmullem1  33168  fedgmullem2  33169  fedgmul  33170  algextdeglem1  33228  algextdeglem4  33231  lmatfvlem  33259  sqsscirc1  33352  cnvordtrestixx  33357  raddcn  33373  xrge0iifhom  33381  xrge0mulc1cn  33385  xrge0tmd  33389  lmlimxrge0  33392  qqhucn  33436  rrhcn  33441  qqtopn  33455  rrhqima  33458  brfae  33710  inelcarsg  33774  cndprobnul  33900  isrrvv  33906  ballotlem1  33949  ballotlem2  33951  ballotlemi1  33965  ballotlemii  33966  ballotlemic  33969  ballotlem1c  33970  ballotlemfrceq  33991  ballotth  34000  ofcs2  34020  signsvtn0  34045  signstfveq0  34052  signsvtp  34058  signsvtn  34059  signsvfpn  34060  signsvfnn  34061  signshf  34063  hashreprin  34096  reprfz1  34100  chtvalz  34105  breprexp  34109  breprexpnat  34110  hgt750lemd  34124  hgt750lem  34127  hgt750lem2  34128  subfacp1lem1  34634  subfacp1lem5  34639  subfacp1lem6  34640  subfaclim  34643  cvmliftlem5  34744  cvmliftlem8  34747  cvmliftlem10  34749  cvmliftlem13  34751  cvmlift2lem6  34763  cvmlift2lem12  34769  problem1  35114  problem2  35115  problem4  35117  quad3  35119  iexpire  35175  sin2h  36942  poimirlem16  36968  poimirlem17  36969  poimirlem18  36970  poimirlem19  36971  poimirlem20  36972  poimirlem21  36973  poimirlem22  36974  poimirlem26  36978  mblfinlem3  36991  ismblfin  36993  itg2addnclem3  37005  iblabsnc  37016  iblmulc2nc  37017  itgmulc2nc  37020  ftc1cnnc  37024  ftc1anclem6  37030  ftc1anclem7  37031  ftc1anclem8  37032  dvasin  37036  fdc  37077  heiborlem4  37146  heiborlem6  37148  dalem24  39032  pmod2iN  39184  cdleme9  39588  cdleme20aN  39644  cdleme22e  39679  cdleme22eALTN  39680  cdleme25cv  39693  cdleme29b  39710  cdlemh1  40150  cdlemh2  40151  cdlemk35  40247  cdlemkid1  40257  12gcd5e1  41335  60gcd7e1  41337  420gcd8e4  41338  12lcm5e60  41340  420lcm8e840  41343  lcm1un  41345  lcm2un  41346  lcm3un  41347  lcm4un  41348  lcm5un  41349  lcm6un  41350  lcm7un  41351  lcm8un  41352  3factsumint1  41353  3factsumint3  41355  lcmineqlem10  41370  3exp7  41385  3lexlogpow5ineq1  41386  3lexlogpow5ineq5  41392  aks4d1p1  41408  5bc2eq10  41425  2ap1caineq  41428  mhphf2  41633  sqmid3api  41658  sqn5i  41660  sqdeccom12  41664  235t711  41668  nn0expgcd  41689  re1m1e0m0  41733  readdlid  41739  remul02  41741  sn-1ticom  41770  sn-mullid  41771  sn-0tie0  41775  sn-mul02  41776  sn-inelr  41801  flt4lem5e  41861  sum9cubes  41877  pellexlem5  42034  reglog1  42097  jm2.23  42198  jm2.27c  42209  lnmlsslnm  42286  lmhmlnmsplit  42292  areaquad  42428  oaomoencom  42530  resqrtvalex  42859  imsqrtvalex  42860  cotrclrcl  42956  inductionexd  43369  hashnzfz2  43543  lhe4.4ex1a  43551  binomcxplemdvsum  43577  binomcxplemnotnn0  43578  binomcxp  43579  sineq0ALT  44161  unirnmapsn  44372  fzisoeu  44469  fsummulc1f  44746  fprodexp  44769  constlimc  44799  sumnnodd  44805  limcresiooub  44817  limcresioolb  44818  cncfshiftioo  45067  fperdvper  45094  dvnmul  45118  dvmptfprod  45120  itgsinexplem1  45129  stoweidlem11  45186  stoweidlem13  45188  stoweidlem26  45201  stoweidlem34  45209  wallispilem4  45243  wallispi2lem1  45246  wallispi2lem2  45247  stirlinglem11  45259  dirkerper  45271  dirkertrigeqlem1  45273  dirkertrigeqlem3  45275  dirkercncflem1  45278  dirkercncflem4  45281  fourierdlem30  45312  fourierdlem32  45314  fourierdlem33  45315  fourierdlem42  45324  fourierdlem46  45327  fourierdlem47  45328  fourierdlem57  45338  fourierdlem60  45341  fourierdlem61  45342  fourierdlem62  45343  fourierdlem68  45349  fourierdlem73  45354  fourierdlem79  45360  fourierdlem89  45370  fourierdlem90  45371  fourierdlem91  45372  fourierdlem96  45377  fourierdlem97  45378  fourierdlem98  45379  fourierdlem99  45380  fourierdlem100  45381  fourierdlem103  45384  fourierdlem104  45385  fourierdlem108  45389  fourierdlem110  45391  fourierdlem113  45394  sqwvfoura  45403  sqwvfourb  45404  fourierswlem  45405  fouriersw  45406  fouriercn  45407  etransclem4  45413  etransclem7  45416  etransclem23  45432  etransclem24  45433  etransclem25  45434  etransclem26  45435  etransclem31  45440  etransclem32  45441  etransclem35  45444  etransclem37  45446  etransclem46  45455  rrndistlt  45465  sge0tsms  45555  sge0xaddlem2  45609  vonioolem2  45856  natlocalincr  46049  upwordsing  46057  tworepnotupword  46059  1t10e1p1e11  46477  deccarry  46478  1fzopredsuc  46491  m1mod0mod1  46496  iccpartgt  46554  fmtno0  46667  fmtno1  46668  fmtnorec2  46670  fmtno2  46677  fmtno3  46678  fmtno4  46679  fmtno5  46684  257prm  46688  fmtnofac1  46697  fmtno4prmfac  46699  fmtno4prmfac193  46700  fmtno4nprmfac193  46701  m2prm  46718  m3prm  46719  flsqrt5  46721  3ndvds4  46722  139prmALT  46723  31prm  46724  127prm  46726  m11nprm  46728  lighneallem2  46733  lighneallem3  46734  3exp4mod41  46743  41prothprmlem1  46744  41prothprmlem2  46745  41prothprm  46746  m1expevenALTV  46774  1oddALTV  46817  6even  46838  8even  46840  2exp340mod341  46860  341fppr2  46861  4fppr1  46862  8exp8mod9  46863  9fppr8  46864  nfermltl8rev  46869  gbpart7  46894  gbpart9  46896  gbpart11  46897  sbgoldbo  46914  bgoldbtbndlem1  46932  tgoldbachlt  46943  altgsumbcALT  47192  lincfsuppcl  47256  linccl  47257  lincvalsn  47260  lincdifsn  47267  lincsum  47272  lincscm  47273  lindslinindimp2lem4  47304  lindslinindsimp2lem5  47305  snlindsntor  47314  lincresunit3lem2  47323  zlmodzxzldeplem3  47345  ldepsnlinc  47351  nn0sumshdiglemA  47467  nn0sumshdiglemB  47468  ackval2  47530  ackval2012  47539  ackval3012  47540  ackval41a  47542  ackval42  47544  ackval42a  47545  affinecomb1  47550  rrx2linest  47590  itschlc0yqe  47608  itsclc0yqsollem1  47610  itscnhlc0xyqsol  47613  itschlc0xyqsol1  47614  itsclquadb  47624  2itscplem2  47627  itscnhlinecirc02plem2  47631  sinh-conventional  47946  onetansqsecsq  47968  cotsqcscsq  47969  mvlraddi  47979  mvrladdi  47980  mvlrmuli  47986  amgmwlem  48011  amgmlemALT  48012