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  21271  gzrngunit  21301  expghm  21336  pzriprng1ALT  21357  chrid  21390  zrhpsgnmhm  21448  psgndiflemA  21465  frlmip  21644  frlmphl  21647  evlsval  21961  mpff  21979  coe1fzgsumdlem  22146  evl1gsumdlem  22196  matvsca2  22251  mattposvs  22278  m2detleiblem3  22452  m2detleiblem4  22453  cpmidpmat  22696  resstopn  23011  cnmpt1res  23501  ressuss  24088  iscusp2  24128  ucnextcn  24130  txmetcnp  24377  rerest  24641  xrtgioo  24643  xrrest  24644  cnmpopc  24770  xrhmeo  24792  clmvs2  24942  clmnegneg  24952  ncvsm1  25003  ncvspi  25005  cphassir  25064  cphipval2  25090  reust  25230  rrxprds  25238  csbren  25248  rrxdsfi  25260  minveclem2  25275  ovolunlem1a  25346  ovolicc2lem4  25370  uniioombllem5  25437  iblabs  25679  iblabsr  25680  iblmulc2  25681  itgmulc2  25684  limcres  25736  dvfval  25747  dvreslem  25759  dvres2lem  25760  dvcnp2  25770  dvcnp2OLD  25771  cpnres  25788  dvmulbr  25790  dvcobr  25798  dvcobrOLD  25799  dveflem  25832  lhop1lem  25867  lhop2  25869  dvcnvrelem2  25872  plyun0  26050  coeeulem  26077  coeeu  26078  dvply1  26137  dvtaylp  26222  taylthlem2  26226  taylth  26227  dvradcnv  26273  pserdvlem2  26281  abelthlem8  26292  abelth  26294  sinhalfpilem  26314  cospi  26323  eulerid  26325  cos2pi  26327  ef2kpi  26329  sinhalfpip  26343  sinhalfpim  26344  coshalfpip  26345  coshalfpim  26346  sincosq3sgn  26351  sincosq4sgn  26352  tangtx  26356  sincos4thpi  26364  sincos6thpi  26366  sineq0  26374  tanregt0  26389  logm1  26438  abslogle  26467  tanarg  26468  logcnlem4  26494  advlogexp  26504  cxpsqrt  26552  dvsqrt  26591  dvcnsqrt  26593  cxpcn3  26598  root1cj  26606  cxpeq  26607  logb1  26616  2logb9irr  26642  sqrt2cxp2logb9e3  26646  ang180lem1  26656  ang180lem2  26657  ang180lem3  26658  lawcos  26663  isosctrlem1  26665  isosctrlem2  26666  quad2  26686  1cubrlem  26688  1cubr  26689  dcubic2  26691  mcubic  26694  binom4  26697  dquartlem1  26698  quart1lem  26702  quart1  26703  quartlem1  26704  asinlem  26715  asinlem2  26716  asinlem3a  26717  acosneg  26734  efiasin  26735  asinsinlem  26738  asinsin  26739  acoscos  26740  asin1  26741  acosbnd  26747  atancj  26757  efiatan  26759  atanlogaddlem  26760  efiatan2  26764  2efiatan  26765  tanatan  26766  cosatan  26768  atantan  26770  atanbndlem  26772  atans2  26778  dvatan  26782  atantayl  26784  atantayl2  26785  log2cnv  26791  log2tlbnd  26792  log2ublem2  26794  log2ublem3  26795  log2ub  26796  birthday  26801  jensenlem1  26834  amgmlem  26837  lgamgulmlem2  26877  lgamgulmlem5  26880  lgambdd  26884  ftalem2  26921  ftalem5  26924  ftalem6  26925  basellem2  26929  basellem3  26930  basellem5  26932  basellem8  26935  basellem9  26936  mule1  26995  ppi1i  27015  musum  27038  ppiublem1  27050  ppiub  27052  chtublem  27059  chtub  27060  dchrptlem1  27112  dchrptlem2  27113  bclbnd  27128  bposlem6  27137  bposlem8  27139  bposlem9  27140  lgsdir2lem1  27173  lgsdir2lem2  27174  lgsdir2lem4  27176  lgsdir2lem5  27177  lgsne0  27183  1lgs  27188  gausslemma2dlem0e  27208  gausslemma2dlem0f  27209  gausslemma2dlem3  27216  gausslemma2d  27222  lgseisenlem1  27223  lgseisenlem2  27224  lgseisenlem3  27225  lgseisenlem4  27226  lgseisen  27227  lgsquadlem1  27228  lgsquadlem2  27229  lgsquad2lem1  27232  lgsquad2lem2  27233  m1lgs  27236  2lgslem3a  27244  2lgslem3b  27245  2lgslem3c  27246  2lgslem3d  27247  2lgsoddprmlem3a  27258  2lgsoddprmlem3b  27259  2lgsoddprmlem3c  27260  2lgsoddprmlem3d  27261  addsqnreup  27291  chebbnd1lem2  27318  chebbnd1lem3  27319  rplogsumlem2  27333  dchrisum0flblem1  27356  dchrisum0re  27361  mulog2sumlem2  27383  chpdifbndlem1  27401  pntpbnd1a  27433  pntpbnd2  27435  pntibndlem2  27439  pntibndlem3  27440  pntlemg  27446  pntlemk  27454  pntlemo  27455  remulscllem1  28110  axsegconlem1  28610  ax5seglem7  28628  axlowdimlem3  28637  axlowdimlem16  28650  axlowdimlem17  28651  elntg2  28678  vdegp1bi  29229  vtxdginducedm1  29235  wlkp1lem1  29365  spthispth  29418  2wlkdlem1  29614  2pthd  29629  clwlkclwwlkfo  29697  3wlkdlem1  29847  3pthd  29862  eucrct2eupth  29933  numclwwlk5  30076  numclwwlk7  30079  frgrregord013  30083  ex-fl  30135  ex-mod  30137  ex-exp  30138  ex-bc  30140  ex-lcm  30146  ex-ind-dvds  30149  vc2OLD  30256  vc0  30262  vcm  30264  nvm1  30353  nvpi  30355  nvmtri  30359  nvge0  30361  ipval3  30397  ipidsq  30398  ip0i  30513  ip1ilem  30514  ip2i  30516  ipdirilem  30517  ipasslem10  30527  siilem1  30539  siii  30541  minvecolem2  30563  hvsubid  30714  hvaddsubval  30721  hvmul2negi  30736  hvadd12i  30745  hv2times  30749  hvnegdii  30750  hvaddcani  30753  hi01  30784  hisubcomi  30792  normlem0  30797  normlem1  30798  normlem3  30800  normlem9  30806  bcseqi  30808  normsqi  30820  norm-ii-i  30825  normsubi  30829  norm3difi  30835  norm3adifii  30836  normpar2i  30844  polid2i  30845  polidi  30846  chdmm2i  31166  chj12i  31210  spanunsni  31267  qlaxr5i  31323  osumcor2i  31332  spansnji  31334  pjadjii  31362  pjinormii  31364  pjsslem  31367  pjpythi  31410  mayete3i  31416  mayetes3i  31417  hoadd12i  31465  honegneg  31494  ho2times  31507  hoaddsubi  31509  hosd1i  31510  hosd2i  31511  honpncani  31515  lnopeq0lem1  31693  lnopunilem1  31698  lnophmlem2  31705  lnfn0i  31730  nmopcoadji  31789  nmopcoadj2i  31790  opsqrlem1  31828  opsqrlem5  31832  opsqrlem6  31833  pjclem3  31885  stadd3i  31936  mddmd2  31997  mdexchi  32023  cvexchlem  32056  atomli  32070  atordi  32072  atabs2i  32090  mdsymlem1  32091  iuninc  32227  suppss2f  32298  mptiffisupp  32350  suppss3  32384  dfdec100  32471  dpfrac1  32493  decdiv10  32497  dpmul100  32498  dp3mul10  32499  dpmul1000  32500  dpexpp1  32509  dpadd2  32511  dpadd  32512  dpmul  32514  dpmul4  32515  threehalves  32516  1mhdrd  32517  pfxlsw2ccat  32551  cyc2fv1  32718  cyc2fv2  32719  cycpmco2lem4  32726  cycpmco2lem5  32727  cyc3fv1  32734  cyc3fv2  32735  cyc3fv3  32736  archirngz  32773  gsumvsca2  32810  nn0omnd  32898  nn0archi  32900  xrge0slmod  32901  opprabs  33038  resssra  33130  lsssra  33131  fedgmullem1  33170  fedgmullem2  33171  fedgmul  33172  algextdeglem1  33230  algextdeglem4  33233  lmatfvlem  33261  sqsscirc1  33354  cnvordtrestixx  33359  raddcn  33375  xrge0iifhom  33383  xrge0mulc1cn  33387  xrge0tmd  33391  lmlimxrge0  33394  qqhucn  33438  rrhcn  33443  qqtopn  33457  rrhqima  33460  brfae  33712  inelcarsg  33776  cndprobnul  33902  isrrvv  33908  ballotlem1  33951  ballotlem2  33953  ballotlemi1  33967  ballotlemii  33968  ballotlemic  33971  ballotlem1c  33972  ballotlemfrceq  33993  ballotth  34002  ofcs2  34022  signsvtn0  34047  signstfveq0  34054  signsvtp  34060  signsvtn  34061  signsvfpn  34062  signsvfnn  34063  signshf  34065  hashreprin  34098  reprfz1  34102  chtvalz  34107  breprexp  34111  breprexpnat  34112  hgt750lemd  34126  hgt750lem  34129  hgt750lem2  34130  subfacp1lem1  34636  subfacp1lem5  34641  subfacp1lem6  34642  subfaclim  34645  cvmliftlem5  34746  cvmliftlem8  34749  cvmliftlem10  34751  cvmliftlem13  34753  cvmlift2lem6  34765  cvmlift2lem12  34771  problem1  35116  problem2  35117  problem4  35119  quad3  35121  iexpire  35177  gg-taylthlem2  35634  sin2h  36945  poimirlem16  36971  poimirlem17  36972  poimirlem18  36973  poimirlem19  36974  poimirlem20  36975  poimirlem21  36976  poimirlem22  36977  poimirlem26  36981  mblfinlem3  36994  ismblfin  36996  itg2addnclem3  37008  iblabsnc  37019  iblmulc2nc  37020  itgmulc2nc  37023  ftc1cnnc  37027  ftc1anclem6  37033  ftc1anclem7  37034  ftc1anclem8  37035  dvasin  37039  fdc  37080  heiborlem4  37149  heiborlem6  37151  dalem24  39035  pmod2iN  39187  cdleme9  39591  cdleme20aN  39647  cdleme22e  39682  cdleme22eALTN  39683  cdleme25cv  39696  cdleme29b  39713  cdlemh1  40153  cdlemh2  40154  cdlemk35  40250  cdlemkid1  40260  12gcd5e1  41338  60gcd7e1  41340  420gcd8e4  41341  12lcm5e60  41343  420lcm8e840  41346  lcm1un  41348  lcm2un  41349  lcm3un  41350  lcm4un  41351  lcm5un  41352  lcm6un  41353  lcm7un  41354  lcm8un  41355  3factsumint1  41356  3factsumint3  41358  lcmineqlem10  41373  3exp7  41388  3lexlogpow5ineq1  41389  3lexlogpow5ineq5  41395  aks4d1p1  41411  5bc2eq10  41428  2ap1caineq  41431  mhphf2  41636  sqmid3api  41661  sqn5i  41663  sqdeccom12  41667  235t711  41671  nn0expgcd  41692  re1m1e0m0  41736  readdlid  41742  remul02  41744  sn-1ticom  41773  sn-mullid  41774  sn-0tie0  41778  sn-mul02  41779  sn-inelr  41804  flt4lem5e  41864  sum9cubes  41880  pellexlem5  42037  reglog1  42100  jm2.23  42201  jm2.27c  42212  lnmlsslnm  42289  lmhmlnmsplit  42295  areaquad  42431  oaomoencom  42533  resqrtvalex  42862  imsqrtvalex  42863  cotrclrcl  42959  inductionexd  43372  hashnzfz2  43546  lhe4.4ex1a  43554  binomcxplemdvsum  43580  binomcxplemnotnn0  43581  binomcxp  43582  sineq0ALT  44164  unirnmapsn  44375  fzisoeu  44472  fsummulc1f  44749  fprodexp  44772  constlimc  44802  sumnnodd  44808  limcresiooub  44820  limcresioolb  44821  cncfshiftioo  45070  fperdvper  45097  dvnmul  45121  dvmptfprod  45123  itgsinexplem1  45132  stoweidlem11  45189  stoweidlem13  45191  stoweidlem26  45204  stoweidlem34  45212  wallispilem4  45246  wallispi2lem1  45249  wallispi2lem2  45250  stirlinglem11  45262  dirkerper  45274  dirkertrigeqlem1  45276  dirkertrigeqlem3  45278  dirkercncflem1  45281  dirkercncflem4  45284  fourierdlem30  45315  fourierdlem32  45317  fourierdlem33  45318  fourierdlem42  45327  fourierdlem46  45330  fourierdlem47  45331  fourierdlem57  45341  fourierdlem60  45344  fourierdlem61  45345  fourierdlem62  45346  fourierdlem68  45352  fourierdlem73  45357  fourierdlem79  45363  fourierdlem89  45373  fourierdlem90  45374  fourierdlem91  45375  fourierdlem96  45380  fourierdlem97  45381  fourierdlem98  45382  fourierdlem99  45383  fourierdlem100  45384  fourierdlem103  45387  fourierdlem104  45388  fourierdlem108  45392  fourierdlem110  45394  fourierdlem113  45397  sqwvfoura  45406  sqwvfourb  45407  fourierswlem  45408  fouriersw  45409  fouriercn  45410  etransclem4  45416  etransclem7  45419  etransclem23  45435  etransclem24  45436  etransclem25  45437  etransclem26  45438  etransclem31  45443  etransclem32  45444  etransclem35  45447  etransclem37  45449  etransclem46  45458  rrndistlt  45468  sge0tsms  45558  sge0xaddlem2  45612  vonioolem2  45859  natlocalincr  46052  upwordsing  46060  tworepnotupword  46062  1t10e1p1e11  46480  deccarry  46481  1fzopredsuc  46494  m1mod0mod1  46499  iccpartgt  46557  fmtno0  46670  fmtno1  46671  fmtnorec2  46673  fmtno2  46680  fmtno3  46681  fmtno4  46682  fmtno5  46687  257prm  46691  fmtnofac1  46700  fmtno4prmfac  46702  fmtno4prmfac193  46703  fmtno4nprmfac193  46704  m2prm  46721  m3prm  46722  flsqrt5  46724  3ndvds4  46725  139prmALT  46726  31prm  46727  127prm  46729  m11nprm  46731  lighneallem2  46736  lighneallem3  46737  3exp4mod41  46746  41prothprmlem1  46747  41prothprmlem2  46748  41prothprm  46749  m1expevenALTV  46777  1oddALTV  46820  6even  46841  8even  46843  2exp340mod341  46863  341fppr2  46864  4fppr1  46865  8exp8mod9  46866  9fppr8  46867  nfermltl8rev  46872  gbpart7  46897  gbpart9  46899  gbpart11  46900  sbgoldbo  46917  bgoldbtbndlem1  46935  tgoldbachlt  46946  altgsumbcALT  47195  lincfsuppcl  47259  linccl  47260  lincvalsn  47263  lincdifsn  47270  lincsum  47275  lincscm  47276  lindslinindimp2lem4  47307  lindslinindsimp2lem5  47308  snlindsntor  47317  lincresunit3lem2  47326  zlmodzxzldeplem3  47348  ldepsnlinc  47354  nn0sumshdiglemA  47470  nn0sumshdiglemB  47471  ackval2  47533  ackval2012  47542  ackval3012  47543  ackval41a  47545  ackval42  47547  ackval42a  47548  affinecomb1  47553  rrx2linest  47593  itschlc0yqe  47611  itsclc0yqsollem1  47613  itscnhlc0xyqsol  47616  itschlc0xyqsol1  47617  itsclquadb  47627  2itscplem2  47630  itscnhlinecirc02plem2  47634  sinh-conventional  47949  onetansqsecsq  47971  cotsqcscsq  47972  mvlraddi  47982  mvrladdi  47983  mvlrmuli  47989  amgmwlem  48014  amgmlemALT  48015