Theorem oveq1i 6660

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

Syntax hints:   = wceq 1483  (class class class)co 6650

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-rex 2918  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-iota 5851  df-fv 5896  df-ov 6653

This theorem is referenced by:  caov12  6862  caov411  6866  omopthlem1  7735  map1  8036  pw2eng  8066  fsuppunbi  8296  cnfcomlem  8596  cnfcom2  8599  infxpenc2  8845  adderpqlem  9776  addassnq  9780  distrnq  9783  halfnq  9798  archnq  9802  addclprlem2  9839  addcmpblnr  9890  ltsrpr  9898  m1m1sr  9914  recexsrlem  9924  sqgt0sr  9927  map2psrpr  9931  axi2m1  9980  axcnre  9985  mul02lem2  10213  addid1  10216  cnegex2  10218  addid2  10219  mvrraddi  10298  mvlladdi  10299  negsubdi  10337  mulneg1  10466  recextlem1  10657  recdiv  10731  divmul13i  10786  mvllmuli  10858  2p2e4  11144  2times  11145  3p2e5  11160  3p3e6  11161  4p2e6  11162  4p3e7  11163  4p4e8  11164  5p2e7  11165  5p3e8  11166  5p4e9  11167  5p5e10OLD  11168  6p2e8  11169  6p3e9  11170  6p4e10OLD  11171  7p2e9  11172  7p3e10OLD  11173  8p2e10OLD  11174  1mhlfehlf  11251  8th4div3  11252  halfpm6th  11253  nneo  11461  dfdecOLD  11495  9p1e10  11496  dfdec10  11497  num0h  11509  numsuc  11511  dec10p  11553  dec10pOLD  11554  numma  11557  nummac  11558  numma2c  11559  numadd  11560  numaddc  11561  nummul2c  11563  decaddci  11580  decsubi  11583  decsubiOLD  11584  decmul1  11585  decmul1OLD  11586  5p5e10  11596  6p4e10  11598  7p3e10  11603  8p2e10  11610  decbin0  11682  decbin2  11683  xmulm1  12111  xadddi2  12127  x2times  12129  elfzp1b  12417  elfzm1b  12418  fz0to4untppr  12442  fz0sn0fz1  12456  fz1fzo0m1  12515  fz0add1fz1  12537  elfz0lmr  12583  fldiv4p1lem1div2  12636  quoremz  12654  quoremnn0ALT  12656  uzrdgxfr  12766  mulexpz  12900  expaddz  12904  sqrecii  12946  sq4e2t8  12962  cu2  12963  i3  12966  iexpcyc  12969  binom2i  12974  binom3  12985  crreczi  12989  discr  13001  3dec  13050  sq10OLD  13051  3decOLD  13053  nn0opthlem1  13055  nn0opth2i  13058  faclbnd  13077  bcm1k  13102  bcp1nk  13104  bcpasc  13108  hashp1i  13191  hashxplem  13220  hashpw  13223  hashfun  13224  hashbc  13237  ccatlid  13369  swrdccatin12  13491  revs1  13514  cats1cat  13606  cats2cat  13607  lsws2  13649  lsws3  13650  lsws4  13651  s3s4  13678  s2s5  13679  s5s2  13680  imre  13848  crim  13855  remullem  13868  cnpart  13980  sqrtneglem  14007  absexpz  14045  absimle  14049  sqreulem  14099  amgm2  14109  iseraltlem2  14413  iseraltlem3  14414  modfsummod  14526  binomlem  14561  binom11  14564  arisum  14592  arisum2  14593  georeclim  14603  geo2sum  14604  mertenslem1  14616  mertens  14618  prodfrec  14627  fprodm1s  14700  fprodp1s  14701  fprodmodd  14728  fallfacfwd  14767  0risefac  14769  bpolydiflem  14785  bpoly2  14788  bpoly3  14789  bpoly4  14790  fsumcube  14791  efzval  14832  resinval  14865  recosval  14866  efi4p  14867  tan0  14881  efival  14882  sinhval  14884  coshval  14885  cosadd  14895  cos2tsin  14909  ef01bndlem  14914  cos1bnd  14917  cos2bnd  14918  absefib  14928  efieq1re  14929  demoivreALT  14931  eirrlem  14932  rpnnen2lem3  14945  rpnnen2lem11  14953  ruclem7  14965  3dvds  15052  3dvdsOLD  15053  3dvdsdec  15054  3dvdsdecOLD  15055  3dvds2dec  15056  3dvds2decOLD  15057  odd2np1  15065  nn0o1gt2  15097  nn0o  15099  pwp1fsum  15114  divalglem2  15118  divalglem9  15124  flodddiv4  15137  m1bits  15162  sadcp1  15177  sadeq  15194  smupp1  15202  smumul  15215  gcdaddmlem  15245  3lcm2e6woprm  15328  nn0gcdsq  15460  phiprmpw  15481  prmdiv  15490  prmdiveq  15491  prmdivdiv  15492  pythagtriplem1  15521  pythagtriplem12  15531  pythagtriplem14  15533  pockthi  15611  infpnlem1  15614  prmreclem4  15623  4sqlem12  15660  4sqlem13  15661  4sqlem19  15667  vdwapun  15678  vdwlem6  15690  0hashbc  15711  prmo2  15744  prmo3  15745  dec5dvds  15768  dec5nprm  15770  dec2nprm  15771  modxai  15772  modxp1i  15774  mod2xnegi  15775  modsubi  15776  gcdmodi  15778  decexp2  15779  decsplit0b  15784  decsplit1  15786  decsplit  15787  decsplit0bOLD  15788  decsplit1OLD  15790  decsplitOLD  15791  karatsuba  15792  karatsubaOLD  15793  2exp8  15796  3exp3  15798  5prm  15815  7prm  15817  11prm  15822  prmlem2  15827  37prm  15828  43prm  15829  83prm  15830  139prm  15831  163prm  15832  317prm  15833  631prm  15834  prmo5  15836  1259lem1  15838  1259lem2  15839  1259lem3  15840  1259lem4  15841  1259lem5  15842  1259prm  15843  2503lem1  15844  2503lem2  15845  2503lem3  15846  2503prm  15847  4001lem1  15848  4001lem2  15849  4001lem3  15850  4001lem4  15851  4001prm  15852  pwsbas  16147  rcaninv  16454  subsubc  16513  xpccatid  16828  subsubm  17357  mulg2  17550  subsubg  17617  oppgmnd  17784  gsumwrev  17796  psgnunilem2  17915  sylow1lem1  18013  subgslw  18031  sylow3  18048  efginvrel2  18140  efgsfo  18152  frgpnabllem1  18276  gsumzaddlem  18321  gsummptfzsplitl  18333  gsummpt1n0  18364  dprdfid  18416  ablfac1lem  18467  pgpfac1lem3  18476  pgpfaclem1  18480  mgpress  18500  srgbinomlem4  18543  opprring  18631  unitsubm  18670  subsubrg  18806  lsslss  18961  evlsval  19519  mpff  19533  coe1fzgsumdlem  19671  evl1gsumdlem  19720  xrsnsgrp  19782  gzrngunit  19812  expghm  19844  chrid  19875  zrhpsgnmhm  19930  psgndiflemA  19947  frlmip  20117  frlmphl  20120  matvsca2  20234  mattposvs  20261  m2detleiblem3  20435  m2detleiblem4  20436  cpmidpmat  20678  resstopn  20990  cnmpt1res  21479  ressuss  22067  iscusp2  22106  ucnextcn  22108  txmetcnp  22352  rerest  22607  xrtgioo  22609  xrrest  22610  cnmpt2pc  22727  xrhmeo  22745  clmvs2  22894  clmnegneg  22904  ncvsm1  22954  ncvspi  22956  cphassir  23015  cphipval2  23040  reust  23169  rrxprds  23177  csbren  23182  minveclem2  23197  ovolunlem1a  23264  ovolicc2lem4  23288  uniioombllem5  23355  iblabs  23595  iblabsr  23596  iblmulc2  23597  itgmulc2  23600  limcres  23650  dvfval  23661  dvreslem  23673  dvres2lem  23674  dvcnp2  23683  cpnres  23700  dvcobr  23709  dveflem  23742  lhop1lem  23776  lhop2  23778  dvcnvrelem2  23781  plyun0  23953  coeeulem  23980  coeeu  23981  dvply1  24039  dvtaylp  24124  taylthlem2  24128  taylth  24129  dvradcnv  24175  pserdvlem2  24182  abelthlem8  24193  abelth  24195  sinhalfpilem  24215  cospi  24224  eulerid  24226  cos2pi  24228  ef2kpi  24230  sinhalfpip  24244  sinhalfpim  24245  coshalfpip  24246  coshalfpim  24247  sincosq3sgn  24252  sincosq4sgn  24253  tangtx  24257  sincos4thpi  24265  sincos6thpi  24267  sineq0  24273  tanregt0  24285  logm1  24335  abslogle  24364  tanarg  24365  logcnlem4  24391  advlogexp  24401  cxpsqrt  24449  dvsqrt  24483  dvcnsqrt  24485  cxpcn3  24489  root1cj  24497  cxpeq  24498  logb1  24507  ang180lem1  24539  ang180lem2  24540  ang180lem3  24541  lawcos  24546  isosctrlem1  24548  isosctrlem2  24549  quad2  24566  1cubrlem  24568  1cubr  24569  dcubic1lem  24570  dcubic2  24571  mcubic  24574  binom4  24577  dquartlem1  24578  quart1lem  24582  quart1  24583  quartlem1  24584  asinlem  24595  asinlem2  24596  asinlem3a  24597  acosneg  24614  efiasin  24615  asinsinlem  24618  asinsin  24619  acoscos  24620  asin1  24621  acosbnd  24627  atancj  24637  efiatan  24639  atanlogaddlem  24640  efiatan2  24644  2efiatan  24645  tanatan  24646  cosatan  24648  atantan  24650  atanbndlem  24652  atans2  24658  dvatan  24662  atantayl  24664  atantayl2  24665  log2cnv  24671  log2tlbnd  24672  log2ublem2  24674  log2ublem3  24675  log2ub  24676  birthday  24681  jensenlem1  24713  amgmlem  24716  lgamgulmlem2  24756  lgamgulmlem5  24759  lgambdd  24763  wilthlem1  24794  ftalem2  24800  ftalem5  24803  ftalem6  24804  basellem2  24808  basellem3  24809  basellem5  24811  basellem8  24814  basellem9  24815  mule1  24874  ppi1i  24894  musum  24917  ppiublem1  24927  ppiublem2  24928  ppiub  24929  chtublem  24936  chtub  24937  dchrptlem1  24989  dchrptlem2  24990  bclbnd  25005  bposlem6  25014  bposlem8  25016  bposlem9  25017  lgslem4  25025  lgsdir2lem1  25050  lgsdir2lem2  25051  lgsdir2lem4  25053  lgsdir2lem5  25054  lgsne0  25060  1lgs  25065  gausslemma2dlem0e  25085  gausslemma2dlem0f  25086  gausslemma2dlem3  25093  gausslemma2d  25099  lgseisenlem1  25100  lgseisenlem2  25101  lgseisenlem3  25102  lgseisenlem4  25103  lgseisen  25104  lgsquadlem1  25105  lgsquadlem2  25106  lgsquad2lem1  25109  lgsquad2lem2  25110  m1lgs  25113  2lgslem3a  25121  2lgslem3b  25122  2lgslem3c  25123  2lgslem3d  25124  2lgsoddprmlem3a  25135  2lgsoddprmlem3b  25136  2lgsoddprmlem3c  25137  2lgsoddprmlem3d  25138  chebbnd1lem2  25159  chebbnd1lem3  25160  rplogsumlem2  25174  dchrisum0flblem1  25197  dchrisum0re  25202  mulog2sumlem2  25224  chpdifbndlem1  25242  pntpbnd1a  25274  pntpbnd2  25276  pntibndlem2  25280  pntibndlem3  25281  pntlemg  25287  pntlemk  25295  pntlemo  25296  axsegconlem1  25797  ax5seglem7  25815  axlowdimlem3  25824  axlowdimlem16  25837  axlowdimlem17  25838  vdegp1bi  26433  vtxdginducedm1  26439  wlkp1lem1  26570  spthispth  26622  2wlkdlem1  26821  2pthd  26836  3wlkdlem1  27019  3pthd  27034  eucrct2eupth  27105  numclwwlk5  27246  numclwwlk7  27249  frgrregord013  27253  ex-fl  27304  ex-mod  27306  ex-exp  27307  ex-bc  27309  ex-lcm  27315  ex-ind-dvds  27318  vc2OLD  27423  vc0  27429  vcm  27431  nvm1  27520  nvpi  27522  nvmtri  27526  nvge0  27528  ipval3  27564  ipidsq  27565  ip0i  27680  ip1ilem  27681  ip2i  27683  ipdirilem  27684  ipasslem10  27694  siilem1  27706  siii  27708  minvecolem2  27731  hvsubid  27883  hvaddsubval  27890  hvmul2negi  27905  hvadd12i  27914  hv2times  27918  hvnegdii  27919  hvaddcani  27922  hi01  27953  hisubcomi  27961  normlem0  27966  normlem1  27967  normlem3  27969  normlem9  27975  bcseqi  27977  normsqi  27989  norm-ii-i  27994  normsubi  27998  norm3difi  28004  norm3adifii  28005  normpar2i  28013  polid2i  28014  polidi  28015  chdmm2i  28337  chj12i  28381  spanunsni  28438  qlaxr5i  28494  osumcor2i  28503  spansnji  28505  pjadjii  28533  pjinormii  28535  pjsslem  28538  pjpythi  28581  mayete3i  28587  mayetes3i  28588  hoadd12i  28636  honegneg  28665  ho2times  28678  hoaddsubi  28680  hosd1i  28681  hosd2i  28682  honpncani  28686  lnopeq0lem1  28864  lnopunilem1  28869  lnophmlem2  28876  lnfn0i  28901  nmopcoadji  28960  nmopcoadj2i  28961  opsqrlem1  28999  opsqrlem5  29003  opsqrlem6  29004  pjclem3  29056  stadd3i  29107  mddmd2  29168  mdexchi  29194  cvexchlem  29227  atomli  29241  atordi  29243  atabs2i  29261  mdsymlem1  29262  iuninc  29379  suppss2f  29439  suppss3  29502  dfdec100  29576  dpfrac1  29599  dpfrac1OLD  29600  decdiv10  29604  dpmul100  29605  dp3mul10  29606  dpmul1000  29607  dpexpp1  29616  dpadd2  29618  dpadd  29619  dpmul  29621  dpmul4  29622  threehalves  29623  1mhdrd  29624  archirngz  29743  gsumvsca2  29783  nn0omnd  29841  nn0archi  29843  xrge0slmod  29844  lmatfvlem  29881  sqsscirc1  29954  cnvordtrestixx  29959  raddcn  29975  xrge0iifhom  29983  xrge0mulc1cn  29987  xrge0tmd  29992  lmlimxrge0  29994  qqhucn  30036  rrhcn  30041  qqtopn  30055  rrhqima  30058  brfae  30311  inelcarsg  30373  cndprobnul  30499  isrrvv  30505  ballotlem1  30548  ballotlem2  30550  ballotlemodife  30559  ballotlemi1  30564  ballotlemii  30565  ballotlemic  30568  ballotlem1c  30569  ballotlemfrceq  30590  ballotth  30599  ofcs2  30622  signsvtn0  30647  signstfveq0  30654  signsvtp  30660  signsvtn  30661  signsvfpn  30662  signsvfnn  30663  signshf  30665  hashreprin  30698  reprfz1  30702  chtvalz  30707  breprexp  30711  breprexpnat  30712  hgt750lemd  30726  hgt750lem  30729  hgt750lem2  30730  subfacp1lem1  31161  subfacp1lem5  31166  subfacp1lem6  31167  subfaclim  31170  cvmliftlem5  31271  cvmliftlem8  31274  cvmliftlem10  31276  cvmliftlem13  31278  cvmlift2lem6  31290  cvmlift2lem12  31296  problem1  31558  problem2  31559  problem2OLD  31560  problem4  31562  quad3  31564  iexpire  31621  sin2h  33399  poimirlem16  33425  poimirlem17  33426  poimirlem18  33427  poimirlem19  33428  poimirlem20  33429  poimirlem21  33430  poimirlem22  33431  poimirlem26  33435  mblfinlem3  33448  ismblfin  33450  itg2addnclem3  33463  iblabsnc  33474  iblmulc2nc  33475  itgmulc2nc  33478  ftc1cnnc  33484  ftc1anclem6  33490  ftc1anclem7  33491  ftc1anclem8  33492  dvasin  33496  fdc  33541  heiborlem4  33613  heiborlem6  33615  dalem24  34983  pmod2iN  35135  cdleme9  35540  cdleme20aN  35597  cdleme22e  35632  cdleme22eALTN  35633  cdleme25cv  35646  cdleme29b  35663  cdlemh1  36103  cdlemh2  36104  cdlemk35  36200  cdlemkid1  36210  pellexlem5  37397  reglog1  37460  jm2.23  37563  jm2.27c  37574  lnmlsslnm  37651  lmhmlnmsplit  37657  cntzsdrg  37772  areaquad  37802  cotrclrcl  38034  inductionexd  38453  hashnzfz2  38520  lhe4.4ex1a  38528  binomcxplemdvsum  38554  binomcxplemnotnn0  38555  binomcxp  38556  sineq0ALT  39173  unirnmapsn  39406  fzisoeu  39514  fz1ssfz0  39524  fsummulc1f  39802  fprodexp  39826  constlimc  39856  sumnnodd  39862  limcresiooub  39874  limcresioolb  39875  cncfshiftioo  40105  fperdvper  40133  dvnmul  40158  dvmptfprod  40160  itgsinexplem1  40169  stoweidlem11  40228  stoweidlem13  40230  stoweidlem26  40243  stoweidlem34  40251  wallispilem4  40285  wallispi2lem1  40288  wallispi2lem2  40289  stirlinglem11  40301  dirkerper  40313  dirkertrigeqlem1  40315  dirkertrigeqlem3  40317  dirkercncflem1  40320  dirkercncflem4  40323  fourierdlem30  40354  fourierdlem32  40356  fourierdlem33  40357  fourierdlem42  40366  fourierdlem46  40369  fourierdlem47  40370  fourierdlem57  40380  fourierdlem60  40383  fourierdlem61  40384  fourierdlem62  40385  fourierdlem68  40391  fourierdlem73  40396  fourierdlem79  40402  fourierdlem89  40412  fourierdlem90  40413  fourierdlem91  40414  fourierdlem96  40419  fourierdlem97  40420  fourierdlem98  40421  fourierdlem99  40422  fourierdlem100  40423  fourierdlem103  40426  fourierdlem104  40427  fourierdlem108  40431  fourierdlem110  40433  fourierdlem113  40436  sqwvfoura  40445  sqwvfourb  40446  fourierswlem  40447  fouriersw  40448  fouriercn  40449  etransclem4  40455  etransclem7  40458  etransclem23  40474  etransclem24  40475  etransclem25  40476  etransclem26  40477  etransclem31  40482  etransclem32  40483  etransclem35  40486  etransclem37  40488  etransclem46  40497  rrxdsfi  40505  rrndistlt  40510  sge0tsms  40597  sge0xaddlem2  40651  vonioolem2  40895  1t10e1p1e11  41319  1t10e1p1e11OLD  41320  deccarry  41321  1fzopredsuc  41334  m1mod0mod1  41339  iccpartgt  41363  pfxccatin12  41425  fmtno0  41452  fmtno1  41453  fmtnorec2  41455  fmtno2  41462  fmtno3  41463  fmtno4  41464  fmtno5  41469  257prm  41473  fmtnofac1  41482  fmtno4prmfac  41484  fmtno4prmfac193  41485  fmtno4nprmfac193  41486  pwdif  41501  m2prm  41505  m3prm  41506  flsqrt5  41509  3ndvds4  41510  139prmALT  41511  31prm  41512  2exp7  41514  127prm  41515  m11nprm  41518  lighneallem2  41523  lighneallem3  41524  3exp4mod41  41533  41prothprmlem1  41534  41prothprmlem2  41535  41prothprm  41536  m1expevenALTV  41560  1oddALTV  41601  6even  41620  8even  41622  gbpart7  41655  gbpart9  41657  gbpart11  41658  sbgoldbo  41675  bgoldbtbndlem1  41693  tgoldbachlt  41704  tgoldbachltOLD  41710  subsubmgm  41797  altgsumbcALT  42131  lincfsuppcl  42202  linccl  42203  lincvalsn  42206  lincdifsn  42213  lincsum  42218  lincscm  42219  lindslinindimp2lem4  42250  lindslinindsimp2lem5  42251  snlindsntor  42260  lincresunit3lem2  42269  zlmodzxzldeplem3  42291  ldepsnlinc  42297  nn0sumshdiglemA  42413  nn0sumshdiglemB  42414  sinh-conventional  42480  onetansqsecsq  42502  cotsqcscsq  42503  mvlraddi  42514  mvrladdi  42516  mvlrmuli  42523  amgmwlem  42548  amgmlemALT  42549