Theorem oveq1i 6559

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

Syntax hints:   = wceq 1475  (class class class)co 6549

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-rex 2902  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-br 4584  df-iota 5768  df-fv 5812  df-ov 6552

This theorem is referenced by:  caov12  6760  caov411  6764  omopthlem1  7622  map1  7921  pw2eng  7951  fsuppunbi  8179  cnfcomlem  8479  cnfcom2  8482  infxpenc2  8728  adderpqlem  9655  addassnq  9659  distrnq  9662  halfnq  9677  archnq  9681  addclprlem2  9718  addcmpblnr  9769  ltsrpr  9777  m1m1sr  9793  recexsrlem  9803  sqgt0sr  9806  map2psrpr  9810  axi2m1  9859  axcnre  9864  mul02lem2  10092  addid1  10095  cnegex2  10097  addid2  10098  mvrraddi  10177  mvlladdi  10178  negsubdi  10216  mulneg1  10345  recextlem1  10536  recdiv  10610  divmul13i  10665  mvllmuli  10737  2p2e4  11021  2times  11022  3p2e5  11037  3p3e6  11038  4p2e6  11039  4p3e7  11040  4p4e8  11041  5p2e7  11042  5p3e8  11043  5p4e9  11044  5p5e10OLD  11045  6p2e8  11046  6p3e9  11047  6p4e10OLD  11048  7p2e9  11049  7p3e10OLD  11050  8p2e10OLD  11051  1mhlfehlf  11128  8th4div3  11129  halfpm6th  11130  nneo  11337  dfdecOLD  11371  9p1e10  11372  dfdec10  11373  num0h  11385  numsuc  11387  dec10p  11429  dec10pOLD  11430  numma  11433  nummac  11434  numma2c  11435  numadd  11436  numaddc  11437  nummul2c  11439  decaddci  11456  decsubi  11459  decsubiOLD  11460  decmul1  11461  decmul1OLD  11462  5p5e10  11472  6p4e10  11474  7p3e10  11479  8p2e10  11486  decbin0  11558  decbin2  11559  xmulm1  11983  xadddi2  11999  x2times  12001  elfzp1b  12286  elfzm1b  12287  fz0to4untppr  12311  fz0sn0fz1  12325  fz1fzo0m1  12383  fldiv4p1lem1div2  12498  quoremz  12516  quoremnn0ALT  12518  uzrdgxfr  12628  mulexpz  12762  expaddz  12766  sqrecii  12808  sq4e2t8  12824  cu2  12825  i3  12828  iexpcyc  12831  binom2i  12836  binom3  12847  crreczi  12851  discr  12863  3dec  12912  sq10OLD  12913  3decOLD  12915  nn0opthlem1  12917  nn0opth2i  12920  faclbnd  12939  bcm1k  12964  bcp1nk  12966  bcpasc  12970  hashp1i  13052  hashxplem  13080  hashpw  13083  hashfun  13084  hashbc  13094  ccatlid  13222  swrdccatin12  13342  revs1  13365  cats1cat  13457  cats2cat  13458  lsws2  13499  lsws3  13500  lsws4  13501  s3s4  13528  s2s5  13529  s5s2  13530  imre  13696  crim  13703  remullem  13716  cnpart  13828  sqrtneglem  13855  absexpz  13893  absimle  13897  sqreulem  13947  amgm2  13957  iseraltlem2  14261  iseraltlem3  14262  modfsummod  14367  binomlem  14400  binom11  14403  arisum  14431  arisum2  14432  georeclim  14442  geo2sum  14443  mertenslem1  14455  mertens  14457  prodfrec  14466  fprodm1s  14539  fprodp1s  14540  fprodmodd  14567  fallfacfwd  14606  0risefac  14608  bpolydiflem  14624  bpoly2  14627  bpoly3  14628  bpoly4  14629  fsumcube  14630  efzval  14671  resinval  14704  recosval  14705  efi4p  14706  tan0  14720  efival  14721  sinhval  14723  coshval  14724  cosadd  14734  cos2tsin  14748  ef01bndlem  14753  cos1bnd  14756  cos2bnd  14757  absefib  14767  efieq1re  14768  demoivreALT  14770  eirrlem  14771  rpnnen2lem3  14784  rpnnen2lem11  14792  ruclem7  14804  3dvds  14890  3dvdsOLD  14891  3dvdsdec  14892  3dvdsdecOLD  14893  3dvds2dec  14894  3dvds2decOLD  14895  odd2np1  14903  nn0o1gt2  14935  nn0o  14937  pwp1fsum  14952  divalglem2  14956  divalglem9  14962  flodddiv4  14975  m1bits  15000  sadcp1  15015  sadeq  15032  smupp1  15040  smumul  15053  gcdaddmlem  15083  3lcm2e6woprm  15166  nn0gcdsq  15298  phiprmpw  15319  prmdiv  15328  prmdiveq  15329  prmdivdiv  15330  pythagtriplem1  15359  pythagtriplem12  15369  pythagtriplem14  15371  pockthi  15449  infpnlem1  15452  prmreclem4  15461  4sqlem12  15498  4sqlem13  15499  4sqlem19  15505  vdwapun  15516  vdwlem6  15528  0hashbc  15549  prmo2  15582  prmo3  15583  dec5dvds  15606  dec5nprm  15608  dec2nprm  15609  modxai  15610  modxp1i  15612  mod2xnegi  15613  modsubi  15614  gcdmodi  15616  decexp2  15617  decsplit0b  15622  decsplit1  15624  decsplit  15625  decsplit0bOLD  15626  decsplit1OLD  15628  decsplitOLD  15629  karatsuba  15630  karatsubaOLD  15631  2exp8  15634  3exp3  15636  5prm  15653  7prm  15655  11prm  15660  prmlem2  15665  37prm  15666  43prm  15667  83prm  15668  139prm  15669  163prm  15670  317prm  15671  631prm  15672  prmo5  15674  1259lem1  15676  1259lem2  15677  1259lem3  15678  1259lem4  15679  1259lem5  15680  1259prm  15681  2503lem1  15682  2503lem2  15683  2503lem3  15684  2503prm  15685  4001lem1  15686  4001lem2  15687  4001lem3  15688  4001lem4  15689  4001prm  15690  pwsbas  15970  rcaninv  16277  subsubc  16336  xpccatid  16651  subsubm  17180  mulg2  17373  subsubg  17440  oppgmnd  17607  gsumwrev  17619  psgnunilem2  17738  sylow1lem1  17836  subgslw  17854  sylow3  17871  efginvrel2  17963  efgsfo  17975  frgpnabllem1  18099  gsumzaddlem  18144  gsummptfzsplitl  18156  gsummpt1n0  18187  dprdfid  18239  ablfac1lem  18290  pgpfac1lem3  18299  pgpfaclem1  18303  mgpress  18323  srgbinomlem4  18366  opprring  18454  unitsubm  18493  subsubrg  18629  lsslss  18782  evlsval  19340  mpff  19354  coe1fzgsumdlem  19492  evl1gsumdlem  19541  xrsnsgrp  19601  gzrngunit  19631  expghm  19663  chrid  19694  zrhpsgnmhm  19749  psgndiflemA  19766  frlmip  19936  frlmphl  19939  matvsca2  20053  mattposvs  20080  m2detleiblem3  20254  m2detleiblem4  20255  cpmidpmat  20497  resstopn  20800  cnmpt1res  21289  ressuss  21877  iscusp2  21916  ucnextcn  21918  txmetcnp  22162  rerest  22415  xrtgioo  22417  xrrest  22418  cnmpt2pc  22535  xrhmeo  22553  clmvs2  22702  clmnegneg  22712  ncvsm1  22762  ncvspi  22764  cphassir  22823  cphipval2  22848  reust  22977  rrxprds  22985  csbren  22990  minveclem2  23005  ovolunlem1a  23071  ovolicc2lem4  23095  uniioombllem5  23161  iblabs  23401  iblabsr  23402  iblmulc2  23403  itgmulc2  23406  limcres  23456  dvfval  23467  dvreslem  23479  dvres2lem  23480  dvcnp2  23489  cpnres  23506  dvcobr  23515  dveflem  23546  lhop1lem  23580  lhop2  23582  dvcnvrelem2  23585  plyun0  23757  coeeulem  23784  coeeu  23785  dvply1  23843  dvtaylp  23928  taylthlem2  23932  taylth  23933  dvradcnv  23979  pserdvlem2  23986  abelthlem8  23997  abelth  23999  sinhalfpilem  24019  cospi  24028  eulerid  24030  cos2pi  24032  ef2kpi  24034  sinhalfpip  24048  sinhalfpim  24049  coshalfpip  24050  coshalfpim  24051  sincosq3sgn  24056  sincosq4sgn  24057  tangtx  24061  sincos4thpi  24069  sincos6thpi  24071  sineq0  24077  tanregt0  24089  logm1  24139  abslogle  24168  tanarg  24169  logcnlem4  24191  advlogexp  24201  cxpsqrt  24249  dvsqrt  24283  dvcnsqrt  24285  cxpcn3  24289  root1cj  24297  cxpeq  24298  logb1  24307  ang180lem1  24339  ang180lem2  24340  ang180lem3  24341  lawcos  24346  isosctrlem1  24348  isosctrlem2  24349  quad2  24366  1cubrlem  24368  1cubr  24369  dcubic1lem  24370  dcubic2  24371  mcubic  24374  binom4  24377  dquartlem1  24378  quart1lem  24382  quart1  24383  quartlem1  24384  asinlem  24395  asinlem2  24396  asinlem3a  24397  acosneg  24414  efiasin  24415  asinsinlem  24418  asinsin  24419  acoscos  24420  asin1  24421  acosbnd  24427  atancj  24437  efiatan  24439  atanlogaddlem  24440  efiatan2  24444  2efiatan  24445  tanatan  24446  cosatan  24448  atantan  24450  atanbndlem  24452  atans2  24458  dvatan  24462  atantayl  24464  atantayl2  24465  log2cnv  24471  log2tlbnd  24472  log2ublem2  24474  log2ublem3  24475  log2ub  24476  birthday  24481  jensenlem1  24513  amgmlem  24516  lgamgulmlem2  24556  lgamgulmlem5  24559  lgambdd  24563  wilthlem1  24594  ftalem2  24600  ftalem5  24603  ftalem6  24604  basellem2  24608  basellem3  24609  basellem5  24611  basellem8  24614  basellem9  24615  mule1  24674  ppi1i  24694  musum  24717  ppiublem1  24727  ppiublem2  24728  ppiub  24729  chtublem  24736  chtub  24737  dchrptlem1  24789  dchrptlem2  24790  bclbnd  24805  bposlem6  24814  bposlem8  24816  bposlem9  24817  lgslem4  24825  lgsdir2lem1  24850  lgsdir2lem2  24851  lgsdir2lem4  24853  lgsdir2lem5  24854  lgsne0  24860  1lgs  24865  gausslemma2dlem0e  24885  gausslemma2dlem0f  24886  gausslemma2dlem3  24893  gausslemma2d  24899  lgseisenlem1  24900  lgseisenlem2  24901  lgseisenlem3  24902  lgseisenlem4  24903  lgseisen  24904  lgsquadlem1  24905  lgsquadlem2  24906  lgsquad2lem1  24909  lgsquad2lem2  24910  m1lgs  24913  2lgslem3a  24921  2lgslem3b  24922  2lgslem3c  24923  2lgslem3d  24924  2lgsoddprmlem3a  24935  2lgsoddprmlem3b  24936  2lgsoddprmlem3c  24937  2lgsoddprmlem3d  24938  chebbnd1lem2  24959  chebbnd1lem3  24960  rplogsumlem2  24974  dchrisum0flblem1  24997  dchrisum0re  25002  mulog2sumlem2  25024  chpdifbndlem1  25042  pntpbnd1a  25074  pntpbnd2  25076  pntibndlem2  25080  pntibndlem3  25081  pntlemg  25087  pntlemk  25095  pntlemo  25096  axsegconlem1  25597  ax5seglem7  25615  axlowdimlem3  25624  axlowdimlem16  25637  axlowdimlem17  25638  fargshiftlem  26162  constr3trllem3  26180  eupares  26502  konigsberg  26514  numclwwlk5  26639  numclwwlk7  26641  frgraregord013  26645  ex-fl  26696  ex-mod  26698  ex-exp  26699  ex-bc  26701  ex-lcm  26707  ex-ind-dvds  26710  vc2OLD  26807  vc0  26813  vcm  26815  nvm1  26904  nvpi  26906  nvmtri  26910  nvge0  26912  ipval3  26948  ipidsq  26949  ip0i  27064  ip1ilem  27065  ip2i  27067  ipdirilem  27068  ipasslem10  27078  siilem1  27090  siii  27092  minvecolem2  27115  hvsubid  27267  hvaddsubval  27274  hvmul2negi  27289  hvadd12i  27298  hv2times  27302  hvnegdii  27303  hvaddcani  27306  hi01  27337  hisubcomi  27345  normlem0  27350  normlem1  27351  normlem3  27353  normlem9  27359  bcseqi  27361  normsqi  27373  norm-ii-i  27378  normsubi  27382  norm3difi  27388  norm3adifii  27389  normpar2i  27397  polid2i  27398  polidi  27399  chdmm2i  27721  chj12i  27765  spanunsni  27822  qlaxr5i  27878  osumcor2i  27887  spansnji  27889  pjadjii  27917  pjinormii  27919  pjsslem  27922  pjpythi  27965  mayete3i  27971  mayetes3i  27972  hoadd12i  28020  honegneg  28049  ho2times  28062  hoaddsubi  28064  hosd1i  28065  hosd2i  28066  honpncani  28070  lnopeq0lem1  28248  lnopunilem1  28253  lnophmlem2  28260  lnfn0i  28285  nmopcoadji  28344  nmopcoadj2i  28345  opsqrlem1  28383  opsqrlem5  28387  opsqrlem6  28388  pjclem3  28440  stadd3i  28491  mddmd2  28552  mdexchi  28578  cvexchlem  28611  atomli  28625  atordi  28627  atabs2i  28645  mdsymlem1  28646  iuninc  28761  suppss2f  28819  suppss3  28890  archirngz  29074  gsumvsca2  29114  nn0omnd  29172  nn0archi  29174  xrge0slmod  29175  lmatfvlem  29209  sqsscirc1  29282  cnvordtrestixx  29287  raddcn  29303  xrge0iifhom  29311  xrge0mulc1cn  29315  xrge0tmd  29320  lmlimxrge0  29322  qqhucn  29364  rrhcn  29369  qqtopn  29383  rrhqima  29386  brfae  29638  inelcarsg  29700  cndprobnul  29826  isrrvv  29832  ballotlem1  29875  ballotlem2  29877  ballotlemodife  29886  ballotlemi1  29891  ballotlemii  29892  ballotlemic  29895  ballotlem1c  29896  ballotlemfrceq  29917  ballotth  29926  ofcs2  29948  signsvtn0  29973  signstfveq0  29980  signsvtp  29986  signsvtn  29987  signsvfpn  29988  signsvfnn  29989  signshf  29991  subfacp1lem1  30415  subfacp1lem5  30420  subfacp1lem6  30421  subfaclim  30424  cvmliftlem5  30525  cvmliftlem8  30528  cvmliftlem10  30530  cvmliftlem13  30532  cvmlift2lem6  30544  cvmlift2lem12  30550  problem1  30812  problem2  30813  problem2OLD  30814  problem4  30816  quad3  30818  iexpire  30874  sin2h  32569  poimirlem16  32595  poimirlem17  32596  poimirlem18  32597  poimirlem19  32598  poimirlem20  32599  poimirlem21  32600  poimirlem22  32601  poimirlem26  32605  mblfinlem3  32618  ismblfin  32620  itg2addnclem3  32633  iblabsnc  32644  iblmulc2nc  32645  itgmulc2nc  32648  ftc1cnnc  32654  ftc1anclem6  32660  ftc1anclem7  32661  ftc1anclem8  32662  dvasin  32666  fdc  32711  heiborlem4  32783  heiborlem6  32785  dalem24  34001  pmod2iN  34153  cdleme9  34558  cdleme20aN  34615  cdleme22e  34650  cdleme22eALTN  34651  cdleme25cv  34664  cdleme29b  34681  cdlemh1  35121  cdlemh2  35122  cdlemk35  35218  cdlemkid1  35228  pellexlem5  36415  reglog1  36478  jm2.23  36581  jm2.27c  36592  lnmlsslnm  36669  lmhmlnmsplit  36675  cntzsdrg  36791  areaquad  36821  cotrclrcl  37053  inductionexd  37473  hashnzfz2  37542  lhe4.4ex1a  37550  binomcxplemdvsum  37576  binomcxplemnotnn0  37577  binomcxp  37578  sineq0ALT  38195  unirnmapsn  38401  fzisoeu  38455  fz1ssfz0  38465  fsummulc1f  38635  fprodexp  38661  constlimc  38691  sumnnodd  38697  limcresiooub  38709  limcresioolb  38710  cncfshiftioo  38778  fperdvper  38808  dvnmul  38833  dvmptfprod  38835  itgsinexplem1  38845  stoweidlem11  38904  stoweidlem13  38906  stoweidlem26  38919  stoweidlem34  38927  wallispilem4  38961  wallispi2lem1  38964  wallispi2lem2  38965  stirlinglem11  38977  dirkerper  38989  dirkertrigeqlem1  38991  dirkertrigeqlem3  38993  dirkercncflem1  38996  dirkercncflem4  38999  fourierdlem30  39030  fourierdlem32  39032  fourierdlem33  39033  fourierdlem42  39042  fourierdlem46  39045  fourierdlem47  39046  fourierdlem57  39056  fourierdlem60  39059  fourierdlem61  39060  fourierdlem62  39061  fourierdlem68  39067  fourierdlem73  39072  fourierdlem79  39078  fourierdlem89  39088  fourierdlem90  39089  fourierdlem91  39090  fourierdlem96  39095  fourierdlem97  39096  fourierdlem98  39097  fourierdlem99  39098  fourierdlem100  39099  fourierdlem103  39102  fourierdlem104  39103  fourierdlem108  39107  fourierdlem110  39109  fourierdlem113  39112  sqwvfoura  39121  sqwvfourb  39122  fourierswlem  39123  fouriersw  39124  fouriercn  39125  etransclem4  39131  etransclem7  39134  etransclem23  39150  etransclem24  39151  etransclem25  39152  etransclem26  39153  etransclem31  39158  etransclem32  39159  etransclem35  39162  etransclem37  39164  etransclem46  39173  rrxdsfi  39181  rrndistlt  39186  sge0tsms  39273  sge0xaddlem2  39327  vonioolem2  39572  1t10e1p1e11  39937  1t10e1p1e11OLD  39938  deccarry  39941  1fzopredsuc  39947  m1mod0mod1  39949  iccpartgt  39965  fmtno0  39990  fmtno1  39991  fmtnorec2  39993  fmtno2  40000  fmtno3  40001  fmtno4  40002  fmtno5  40007  257prm  40011  fmtnofac1  40020  fmtno4prmfac  40022  fmtno4prmfac193  40023  fmtno4nprmfac193  40024  pwdif  40039  m2prm  40043  m3prm  40044  flsqrt5  40047  3ndvds4  40048  139prmALT  40049  31prm  40050  2exp7  40052  127prm  40053  m11nprm  40056  lighneallem2  40061  lighneallem3  40062  3exp4mod41  40071  41prothprmlem1  40072  41prothprmlem2  40073  41prothprm  40074  m1expevenALTV  40098  1oddALTV  40139  6even  40158  8even  40160  gbpart7  40189  gbpart9  40191  gbpart11  40192  bgoldbtbndlem1  40221  tgoldbachlt  40230  tgoldbachltOLD  40237  pfxccatin12  40288  elfz0lmr  40367  vdegp1bi-av  40753  1wlkp1lem1  40882  sPthisPth  40932  21wlkdlem1  41132  2pthd  41147  31wlkdlem1  41326  3pthd  41341  eucrct2eupth  41413  av-numclwwlk5  41542  av-numclwwlk7  41545  av-frgraregord013  41549  subsubmgm  41587  altgsumbcALT  41924  lincfsuppcl  41996  linccl  41997  lincvalsn  42000  lincdifsn  42007  lincsum  42012  lincscm  42013  lindslinindimp2lem4  42044  lindslinindsimp2lem5  42045  snlindsntor  42054  lincresunit3lem2  42063  zlmodzxzldeplem3  42085  ldepsnlinc  42091  nn0sumshdiglemA  42211  nn0sumshdiglemB  42212  sinh-conventional  42279  onetansqsecsq  42301  cotsqcscsq  42302  dpfrac1  42312  dpfrac1OLD  42313  mvlraddi  42323  mvrladdi  42325  mvlrmuli  42332  amgmwlem  42357  amgmlemALT  42358