Theorem oveq1i 7440

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

Syntax hints:   = wceq 1536  (class class class)co 7430

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-iota 6515  df-fv 6570  df-ov 7433

This theorem is referenced by:  caov12  7660  caov411  7664  omopthlem1  8695  map1  9078  pw2eng  9116  fsuppunbi  9426  cnfcomlem  9736  cnfcom2  9739  infxpenc2  10059  adderpqlem  10991  addassnq  10995  distrnq  10998  halfnq  11013  archnq  11017  addclprlem2  11054  addcmpblnr  11106  ltsrpr  11114  m1m1sr  11130  recexsrlem  11140  sqgt0sr  11143  map2psrpr  11147  axi2m1  11196  axcnre  11201  mul02lem2  11435  addrid  11438  cnegex2  11440  addlid  11441  mvrraddi  11522  mvrladdi  11523  mvlladdi  11524  negsubdi  11562  mulneg1  11696  recextlem1  11890  recdiv  11970  divmul13i  12025  mvllmuli  12097  2p2e4  12398  2times  12399  1p2e3  12406  3p2e5  12414  3p3e6  12415  4p2e6  12416  4p3e7  12417  4p4e8  12418  5p2e7  12419  5p3e8  12420  5p4e9  12421  6p2e8  12422  6p3e9  12423  7p2e9  12424  1mhlfehlf  12482  8th4div3  12483  halfpm6th  12484  nneo  12699  9p1e10  12732  dfdec10  12733  num0h  12742  numsuc  12744  dec10p  12773  numma  12774  nummac  12775  numma2c  12776  numadd  12777  numaddc  12778  nummul2c  12780  decaddci  12791  decsubi  12793  5p5e10  12801  6p4e10  12802  7p3e10  12805  8p2e10  12810  decbin0  12870  decbin2  12871  xmulm1  13319  xadddi2  13335  x2times  13337  elfzp1b  13637  elfzm1b  13638  fz0dif1  13642  fz1ssfz0  13659  fz0to4untppr  13666  fz0to5un2tp  13667  fz0sn0fz1  13681  fz0add1fz1  13770  elfz0lmr  13817  fldiv4p1lem1div2  13871  quoremz  13891  quoremnn0ALT  13893  uzrdgxfr  14004  mulexpz  14139  expaddz  14143  sqrecii  14218  sq4e2t8  14234  cu2  14235  i3  14238  iexpcyc  14242  binom2i  14247  binom3  14259  crreczi  14263  discr  14275  3dec  14301  nn0opthlem1  14303  nn0opth2i  14306  faclbnd  14325  bcp1nk  14352  bcpasc  14356  hashp1i  14438  hashxplem  14468  hashpw  14471  hashfun  14472  hashbc  14488  hash7g  14521  ccatlid  14620  pfxccatin12lem2c  14764  revs1  14799  cats1cat  14896  cats2cat  14897  lsws2  14939  lsws3  14940  lsws4  14941  s3s4  14968  s2s5  14969  s5s2  14970  imre  15143  crim  15150  remullem  15163  cnpart  15275  sqrtneglem  15301  absexpz  15340  absimle  15344  sqreulem  15394  amgm2  15404  iseraltlem2  15715  iseraltlem3  15716  modfsummod  15826  binomlem  15861  binom11  15864  arisum  15892  arisum2  15893  pwdif  15900  georeclim  15904  geo2sum  15905  mertenslem1  15916  mertens  15918  prodfrec  15927  fprodm1s  16002  fprodp1s  16003  fprodmodd  16029  fallfacfwd  16068  0risefac  16070  bpolydiflem  16086  bpoly2  16089  bpoly3  16090  bpoly4  16091  fsumcube  16092  efzval  16134  resinval  16167  recosval  16168  efi4p  16169  tan0  16183  efival  16184  sinhval  16186  coshval  16187  cosadd  16197  cos2tsin  16211  ef01bndlem  16216  cos1bnd  16219  cos2bnd  16220  absefib  16230  efieq1re  16231  demoivreALT  16233  eirrlem  16236  rpnnen2lem3  16248  rpnnen2lem11  16256  ruclem7  16268  3dvds  16364  3dvdsdec  16365  3dvds2dec  16366  odd2np1  16374  nn0o1gt2  16414  nn0o  16416  pwp1fsum  16424  divalglem2  16428  divalglem9  16434  5ndvds3  16446  5ndvds6  16447  flodddiv4  16448  m1bits  16473  sadcp1  16488  sadeq  16505  smupp1  16513  smumul  16526  gcdaddmlem  16557  nn0expgcd  16597  3lcm2e6woprm  16648  nn0gcdsq  16785  phiprmpw  16809  prmdiv  16818  prmdiveq  16819  pythagtriplem1  16849  pythagtriplem12  16859  pythagtriplem14  16861  pockthi  16940  infpnlem1  16943  prmreclem4  16952  4sqlem12  16989  4sqlem13  16990  4sqlem19  16996  vdwapun  17007  vdwlem6  17019  0hashbc  17040  prmo2  17073  prmo3  17074  dec5dvds  17097  dec5nprm  17099  dec2nprm  17100  modxai  17101  modxp1i  17103  mod2xnegi  17104  modsubi  17105  gcdmodi  17107  decexp2  17108  decsplit0b  17113  decsplit1  17115  decsplit  17116  karatsuba  17117  2exp7  17121  2exp8  17122  3exp3  17125  5prm  17142  7prm  17144  11prm  17148  prmlem2  17153  37prm  17154  43prm  17155  83prm  17156  139prm  17157  163prm  17158  317prm  17159  631prm  17160  prmo5  17162  1259lem1  17164  1259lem2  17165  1259lem3  17166  1259lem4  17167  1259lem5  17168  2503lem1  17170  2503lem2  17171  2503lem3  17172  2503prm  17173  4001lem1  17174  4001lem2  17175  4001lem3  17176  4001lem4  17177  4001prm  17178  pwsbas  17533  rcaninv  17841  subsubc  17903  xpccatid  18243  subsubmgm  18735  subsubm  18841  smndex2dnrinv  18940  mulg2  19113  subsubg  19179  oppgmnd  19387  gsumwrev  19399  psgnunilem2  19527  sylow1lem1  19630  subgslw  19648  sylow3  19665  efginvrel2  19759  efgsfo  19771  frgpnabllem1  19905  gsumzaddlem  19953  gsummptfzsplitl  19965  gsummpt1n0  19997  dprdfid  20051  ablfac1lem  20102  pgpfac1lem3  20111  pgpfaclem1  20115  ablsimpgfindlem1  20141  mgpress  20166  mgpressOLD  20167  srgbinomlem4  20246  opprrng  20361  unitsubm  20402  subsubrng  20579  subsubrg  20614  cntzsdrg  20819  subdrgint  20820  lsslss  20976  xrsnsgrp  21437  gzrngunit  21468  expghm  21503  pzriprng1ALT  21524  chrid  21557  zrhpsgnmhm  21619  psgndiflemA  21636  frlmip  21815  frlmphl  21818  evlsval  22127  mpff  22145  coe1fzgsumdlem  22322  evl1gsumdlem  22375  matvsca2  22449  mattposvs  22476  m2detleiblem3  22650  m2detleiblem4  22651  cpmidpmat  22894  resstopn  23209  cnmpt1res  23699  ressuss  24286  iscusp2  24326  ucnextcn  24328  txmetcnp  24575  rerest  24839  xrtgioo  24841  xrrest  24842  cnmpopc  24968  xrhmeo  24990  clmvs2  25140  clmnegneg  25150  ncvsm1  25201  ncvspi  25203  cphassir  25262  cphipval2  25288  reust  25428  rrxprds  25436  csbren  25446  rrxdsfi  25458  minveclem2  25473  ovolunlem1a  25544  ovolicc2lem4  25568  uniioombllem5  25635  iblabs  25878  iblabsr  25879  iblmulc2  25880  itgmulc2  25883  limcres  25935  dvfval  25946  dvreslem  25958  dvres2lem  25959  dvcnp2  25969  dvcnp2OLD  25970  cpnres  25987  dvmulbr  25989  dvcobr  25997  dvcobrOLD  25998  dveflem  26031  lhop1lem  26066  lhop2  26068  dvcnvrelem2  26071  plyun0  26250  coeeulem  26277  coeeu  26278  dvply1  26339  dvtaylp  26426  taylthlem2  26430  taylthlem2OLD  26431  taylth  26432  dvradcnv  26478  pserdvlem2  26486  abelthlem8  26497  abelth  26499  sinhalfpilem  26519  cospi  26528  eulerid  26530  cos2pi  26532  ef2kpi  26534  sinhalfpip  26548  sinhalfpim  26549  coshalfpip  26550  coshalfpim  26551  sincosq3sgn  26556  sincosq4sgn  26557  tangtx  26561  sincos4thpi  26569  sincos6thpi  26572  sineq0  26580  tanregt0  26595  logm1  26645  abslogle  26674  tanarg  26675  logcnlem4  26701  advlogexp  26711  cxpsqrt  26759  dvsqrt  26798  dvcnsqrt  26800  cxpcn3  26805  root1cj  26813  cxpeq  26814  logb1  26826  2logb9irr  26852  sqrt2cxp2logb9e3  26856  ang180lem1  26866  ang180lem2  26867  ang180lem3  26868  lawcos  26873  isosctrlem1  26875  isosctrlem2  26876  quad2  26896  1cubrlem  26898  1cubr  26899  dcubic2  26901  mcubic  26904  binom4  26907  dquartlem1  26908  quart1lem  26912  quart1  26913  quartlem1  26914  asinlem  26925  asinlem2  26926  asinlem3a  26927  acosneg  26944  efiasin  26945  asinsinlem  26948  asinsin  26949  acoscos  26950  asin1  26951  acosbnd  26957  atancj  26967  efiatan  26969  atanlogaddlem  26970  efiatan2  26974  2efiatan  26975  tanatan  26976  cosatan  26978  atantan  26980  atanbndlem  26982  atans2  26988  dvatan  26992  atantayl  26994  atantayl2  26995  log2cnv  27001  log2tlbnd  27002  log2ublem2  27004  log2ublem3  27005  log2ub  27006  birthday  27011  jensenlem1  27044  amgmlem  27047  lgamgulmlem2  27087  lgamgulmlem5  27090  lgambdd  27094  ftalem2  27131  ftalem5  27134  ftalem6  27135  basellem2  27139  basellem3  27140  basellem5  27142  basellem8  27145  basellem9  27146  mule1  27205  ppi1i  27225  musum  27248  ppiublem1  27260  ppiub  27262  chtublem  27269  chtub  27270  dchrptlem1  27322  dchrptlem2  27323  bclbnd  27338  bposlem6  27347  bposlem8  27349  bposlem9  27350  lgsdir2lem1  27383  lgsdir2lem2  27384  lgsdir2lem4  27386  lgsdir2lem5  27387  lgsne0  27393  1lgs  27398  gausslemma2dlem0e  27418  gausslemma2dlem0f  27419  gausslemma2dlem3  27426  gausslemma2d  27432  lgseisenlem1  27433  lgseisenlem2  27434  lgseisenlem3  27435  lgseisenlem4  27436  lgseisen  27437  lgsquadlem1  27438  lgsquadlem2  27439  lgsquad2lem1  27442  lgsquad2lem2  27443  m1lgs  27446  2lgslem3a  27454  2lgslem3b  27455  2lgslem3c  27456  2lgslem3d  27457  2lgsoddprmlem3a  27468  2lgsoddprmlem3b  27469  2lgsoddprmlem3c  27470  2lgsoddprmlem3d  27471  addsqnreup  27501  chebbnd1lem2  27528  chebbnd1lem3  27529  rplogsumlem2  27543  dchrisum0flblem1  27566  dchrisum0re  27571  mulog2sumlem2  27593  chpdifbndlem1  27611  pntpbnd1a  27643  pntpbnd2  27645  pntibndlem2  27649  pntibndlem3  27650  pntlemg  27656  pntlemk  27664  pntlemo  27665  no2times  28415  zseo  28420  remulscllem1  28446  axsegconlem1  28946  ax5seglem7  28964  axlowdimlem3  28973  axlowdimlem16  28986  axlowdimlem17  28987  elntg2  29014  vdegp1bi  29569  vtxdginducedm1  29575  wlkp1lem1  29705  spthispth  29758  2wlkdlem1  29954  2pthd  29969  clwlkclwwlkfo  30037  3wlkdlem1  30187  3pthd  30202  eucrct2eupth  30273  numclwwlk5  30416  numclwwlk7  30419  frgrregord013  30423  ex-fl  30475  ex-mod  30477  ex-exp  30478  ex-bc  30480  ex-lcm  30486  ex-ind-dvds  30489  vc2OLD  30596  vc0  30602  vcm  30604  nvm1  30693  nvpi  30695  nvmtri  30699  nvge0  30701  ipval3  30737  ipidsq  30738  ip0i  30853  ip1ilem  30854  ip2i  30856  ipdirilem  30857  ipasslem10  30867  siilem1  30879  siii  30881  minvecolem2  30903  hvsubid  31054  hvaddsubval  31061  hvmul2negi  31076  hvadd12i  31085  hv2times  31089  hvnegdii  31090  hvaddcani  31093  hi01  31124  hisubcomi  31132  normlem0  31137  normlem1  31138  normlem3  31140  normlem9  31146  bcseqi  31148  normsqi  31160  norm-ii-i  31165  normsubi  31169  norm3difi  31175  norm3adifii  31176  normpar2i  31184  polid2i  31185  polidi  31186  chdmm2i  31506  chj12i  31550  spanunsni  31607  qlaxr5i  31663  osumcor2i  31672  spansnji  31674  pjadjii  31702  pjinormii  31704  pjsslem  31707  pjpythi  31750  mayete3i  31756  mayetes3i  31757  hoadd12i  31805  honegneg  31834  ho2times  31847  hoaddsubi  31849  hosd1i  31850  hosd2i  31851  honpncani  31855  lnopeq0lem1  32033  lnopunilem1  32038  lnophmlem2  32045  lnfn0i  32070  nmopcoadji  32129  nmopcoadj2i  32130  opsqrlem1  32168  opsqrlem5  32172  opsqrlem6  32173  pjclem3  32225  stadd3i  32276  mddmd2  32337  mdexchi  32363  cvexchlem  32396  atomli  32410  atordi  32412  atabs2i  32430  mdsymlem1  32431  iuninc  32580  suppss2f  32654  mptiffisupp  32707  suppss3  32741  dfdec100  32836  dpfrac1  32858  decdiv10  32862  dpmul100  32863  dp3mul10  32864  dpmul1000  32865  dpexpp1  32874  dpadd2  32876  dpadd  32877  dpmul  32879  dpmul4  32880  threehalves  32881  1mhdrd  32882  pfxlsw2ccat  32919  ccatws1f1olast  32921  chnub  32985  cyc2fv1  33123  cyc2fv2  33124  cycpmco2lem4  33131  cycpmco2lem5  33132  cyc3fv1  33139  cyc3fv2  33140  cyc3fv3  33141  archirngz  33178  gsumvsca2  33215  elrgspnlem4  33234  nn0omnd  33352  nn0archi  33354  xrge0slmod  33355  opprabs  33489  resssra  33616  lsssra  33617  fedgmullem1  33656  fedgmullem2  33657  fedgmul  33658  fldgenfldext  33692  algextdeglem1  33722  algextdeglem4  33725  constrrtcclem  33739  2sqr3minply  33752  lmatfvlem  33775  sqsscirc1  33868  cnvordtrestixx  33873  raddcn  33889  xrge0iifhom  33897  xrge0mulc1cn  33901  xrge0tmd  33905  lmlimxrge0  33908  qqhucn  33954  rrhcn  33959  qqtopn  33973  rrhqima  33976  brfae  34228  inelcarsg  34292  cndprobnul  34418  isrrvv  34424  ballotlem1  34467  ballotlem2  34469  ballotlemi1  34483  ballotlemii  34484  ballotlemic  34487  ballotlem1c  34488  ballotlemfrceq  34509  ballotth  34518  ofcs2  34538  signsvtn0  34563  signstfveq0  34570  signsvtp  34576  signsvtn  34577  signsvfpn  34578  signsvfnn  34579  signshf  34581  hashreprin  34613  reprfz1  34617  chtvalz  34622  breprexp  34626  breprexpnat  34627  hgt750lemd  34641  hgt750lem  34644  hgt750lem2  34645  subfacp1lem1  35163  subfacp1lem5  35168  subfacp1lem6  35169  subfaclim  35172  cvmliftlem5  35273  cvmliftlem8  35276  cvmliftlem10  35278  cvmliftlem13  35280  cvmlift2lem6  35292  cvmlift2lem12  35298  problem1  35649  problem2  35650  problem4  35652  quad3  35654  iexpire  35714  itgeq12i  36187  sin2h  37596  poimirlem16  37622  poimirlem17  37623  poimirlem18  37624  poimirlem19  37625  poimirlem20  37626  poimirlem21  37627  poimirlem22  37628  poimirlem26  37632  mblfinlem3  37645  ismblfin  37647  itg2addnclem3  37659  iblabsnc  37670  iblmulc2nc  37671  itgmulc2nc  37674  ftc1cnnc  37678  ftc1anclem6  37684  ftc1anclem7  37685  ftc1anclem8  37686  dvasin  37690  fdc  37731  heiborlem4  37800  heiborlem6  37802  dalem24  39679  pmod2iN  39831  cdleme9  40235  cdleme20aN  40291  cdleme22e  40326  cdleme22eALTN  40327  cdleme25cv  40340  cdleme29b  40357  cdlemh1  40797  cdlemh2  40798  cdlemk35  40894  cdlemkid1  40904  12gcd5e1  41984  60gcd7e1  41986  420gcd8e4  41987  12lcm5e60  41989  420lcm8e840  41992  lcm1un  41994  lcm2un  41995  lcm3un  41996  lcm4un  41997  lcm5un  41998  lcm6un  41999  lcm7un  42000  lcm8un  42001  3factsumint1  42002  3factsumint3  42004  lcmineqlem10  42019  3exp7  42034  3lexlogpow5ineq1  42035  3lexlogpow5ineq5  42041  aks4d1p1  42057  5bc2eq10  42123  2ap1caineq  42126  aks5lem3a  42170  aks5lem7  42181  sqmid3api  42296  sqn5i  42298  sqdeccom12  42302  235t711  42317  cxpi11d  42357  re1m1e0m0  42403  readdlid  42409  remul02  42411  sn-1ticom  42440  sn-mullid  42441  sn-0tie0  42445  sn-mul02  42446  sn-inelr  42473  mhphf2  42584  flt4lem5e  42642  sum9cubes  42658  pellexlem5  42820  reglog1  42883  jm2.23  42984  jm2.27c  42995  lnmlsslnm  43069  lmhmlnmsplit  43075  areaquad  43204  oaomoencom  43306  resqrtvalex  43634  imsqrtvalex  43635  cotrclrcl  43731  inductionexd  44144  hashnzfz2  44316  lhe4.4ex1a  44324  binomcxplemdvsum  44350  binomcxplemnotnn0  44351  binomcxp  44352  sineq0ALT  44934  unirnmapsn  45156  fzisoeu  45250  fsummulc1f  45526  fprodexp  45549  constlimc  45579  sumnnodd  45585  limcresiooub  45597  limcresioolb  45598  cncfshiftioo  45847  fperdvper  45874  dvnmul  45898  dvmptfprod  45900  itgsinexplem1  45909  stoweidlem11  45966  stoweidlem13  45968  stoweidlem26  45981  stoweidlem34  45989  wallispilem4  46023  wallispi2lem1  46026  wallispi2lem2  46027  stirlinglem11  46039  dirkerper  46051  dirkertrigeqlem1  46053  dirkertrigeqlem3  46055  dirkercncflem1  46058  dirkercncflem4  46061  fourierdlem30  46092  fourierdlem32  46094  fourierdlem33  46095  fourierdlem42  46104  fourierdlem46  46107  fourierdlem47  46108  fourierdlem57  46118  fourierdlem60  46121  fourierdlem61  46122  fourierdlem62  46123  fourierdlem68  46129  fourierdlem73  46134  fourierdlem79  46140  fourierdlem89  46150  fourierdlem90  46151  fourierdlem91  46152  fourierdlem96  46157  fourierdlem97  46158  fourierdlem98  46159  fourierdlem99  46160  fourierdlem100  46161  fourierdlem103  46164  fourierdlem104  46165  fourierdlem108  46169  fourierdlem110  46171  fourierdlem113  46174  sqwvfoura  46183  sqwvfourb  46184  fourierswlem  46185  fouriersw  46186  fouriercn  46187  etransclem4  46193  etransclem7  46196  etransclem23  46212  etransclem24  46213  etransclem25  46214  etransclem26  46215  etransclem31  46220  etransclem32  46221  etransclem35  46224  etransclem37  46226  etransclem46  46235  rrndistlt  46245  sge0tsms  46335  sge0xaddlem2  46389  vonioolem2  46636  natlocalincr  46829  upwordsing  46837  tworepnotupword  46839  1t10e1p1e11  47259  deccarry  47260  1fzopredsuc  47273  ceil5half3  47279  minusmodnep2tmod  47292  m1mod0mod1  47293  iccpartgt  47351  fmtno0  47464  fmtno1  47465  fmtnorec2  47467  fmtno2  47474  fmtno3  47475  fmtno4  47476  fmtno5  47481  257prm  47485  fmtnofac1  47494  fmtno4prmfac  47496  fmtno4prmfac193  47497  fmtno4nprmfac193  47498  m2prm  47515  m3prm  47516  flsqrt5  47518  3ndvds4  47519  139prmALT  47520  31prm  47521  127prm  47523  m11nprm  47525  lighneallem2  47530  lighneallem3  47531  3exp4mod41  47540  41prothprmlem1  47541  41prothprmlem2  47542  41prothprm  47543  m1expevenALTV  47571  1oddALTV  47614  6even  47635  8even  47637  2exp340mod341  47657  341fppr2  47658  4fppr1  47659  8exp8mod9  47660  9fppr8  47661  nfermltl8rev  47666  gbpart7  47691  gbpart9  47693  gbpart11  47694  sbgoldbo  47711  bgoldbtbndlem1  47729  tgoldbachlt  47740  altgsumbcALT  48197  lincfsuppcl  48258  linccl  48259  lincvalsn  48262  lincdifsn  48269  lincsum  48274  lincscm  48275  lindslinindimp2lem4  48306  lindslinindsimp2lem5  48307  snlindsntor  48316  lincresunit3lem2  48325  zlmodzxzldeplem3  48347  ldepsnlinc  48353  nn0sumshdiglemA  48468  nn0sumshdiglemB  48469  ackval2  48531  ackval2012  48540  ackval3012  48541  ackval41a  48543  ackval42  48545  ackval42a  48546  affinecomb1  48551  rrx2linest  48591  itschlc0yqe  48609  itsclc0yqsollem1  48611  itscnhlc0xyqsol  48614  itschlc0xyqsol1  48615  itsclquadb  48625  2itscplem2  48628  itscnhlinecirc02plem2  48632  sinh-conventional  48969  onetansqsecsq  48991  cotsqcscsq  48992  mvlraddi  49001  mvlrmuli  49007  amgmwlem  49032  amgmlemALT  49033