Theorem oveq1i 7458

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

Syntax hints:   = wceq 1537  (class class class)co 7448

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-iota 6525  df-fv 6581  df-ov 7451

This theorem is referenced by:  caov12  7678  caov411  7682  omopthlem1  8715  map1  9105  pw2eng  9144  fsuppunbi  9458  cnfcomlem  9768  cnfcom2  9771  infxpenc2  10091  adderpqlem  11023  addassnq  11027  distrnq  11030  halfnq  11045  archnq  11049  addclprlem2  11086  addcmpblnr  11138  ltsrpr  11146  m1m1sr  11162  recexsrlem  11172  sqgt0sr  11175  map2psrpr  11179  axi2m1  11228  axcnre  11233  mul02lem2  11467  addrid  11470  cnegex2  11472  addlid  11473  mvrraddi  11553  mvlladdi  11554  negsubdi  11592  mulneg1  11726  recextlem1  11920  recdiv  12000  divmul13i  12055  mvllmuli  12127  2p2e4  12428  2times  12429  1p2e3  12436  3p2e5  12444  3p3e6  12445  4p2e6  12446  4p3e7  12447  4p4e8  12448  5p2e7  12449  5p3e8  12450  5p4e9  12451  6p2e8  12452  6p3e9  12453  7p2e9  12454  1mhlfehlf  12512  8th4div3  12513  halfpm6th  12514  nneo  12727  9p1e10  12760  dfdec10  12761  num0h  12770  numsuc  12772  dec10p  12801  numma  12802  nummac  12803  numma2c  12804  numadd  12805  numaddc  12806  nummul2c  12808  decaddci  12819  decsubi  12821  5p5e10  12829  6p4e10  12830  7p3e10  12833  8p2e10  12838  decbin0  12898  decbin2  12899  xmulm1  13343  xadddi2  13359  x2times  13361  elfzp1b  13661  elfzm1b  13662  fz1ssfz0  13680  fz0to4untppr  13687  fz0to5un2tp  13688  fz0sn0fz1  13702  fz0add1fz1  13786  elfz0lmr  13832  fldiv4p1lem1div2  13886  quoremz  13906  quoremnn0ALT  13908  uzrdgxfr  14018  mulexpz  14153  expaddz  14157  sqrecii  14232  sq4e2t8  14248  cu2  14249  i3  14252  iexpcyc  14256  binom2i  14261  binom3  14273  crreczi  14277  discr  14289  3dec  14315  nn0opthlem1  14317  nn0opth2i  14320  faclbnd  14339  bcp1nk  14366  bcpasc  14370  hashp1i  14452  hashxplem  14482  hashpw  14485  hashfun  14486  hashbc  14502  hash7g  14535  ccatlid  14634  pfxccatin12lem2c  14778  revs1  14813  cats1cat  14910  cats2cat  14911  lsws2  14953  lsws3  14954  lsws4  14955  s3s4  14982  s2s5  14983  s5s2  14984  imre  15157  crim  15164  remullem  15177  cnpart  15289  sqrtneglem  15315  absexpz  15354  absimle  15358  sqreulem  15408  amgm2  15418  iseraltlem2  15731  iseraltlem3  15732  modfsummod  15842  binomlem  15877  binom11  15880  arisum  15908  arisum2  15909  pwdif  15916  georeclim  15920  geo2sum  15921  mertenslem1  15932  mertens  15934  prodfrec  15943  fprodm1s  16018  fprodp1s  16019  fprodmodd  16045  fallfacfwd  16084  0risefac  16086  bpolydiflem  16102  bpoly2  16105  bpoly3  16106  bpoly4  16107  fsumcube  16108  efzval  16150  resinval  16183  recosval  16184  efi4p  16185  tan0  16199  efival  16200  sinhval  16202  coshval  16203  cosadd  16213  cos2tsin  16227  ef01bndlem  16232  cos1bnd  16235  cos2bnd  16236  absefib  16246  efieq1re  16247  demoivreALT  16249  eirrlem  16252  rpnnen2lem3  16264  rpnnen2lem11  16272  ruclem7  16284  3dvds  16379  3dvdsdec  16380  3dvds2dec  16381  odd2np1  16389  nn0o1gt2  16429  nn0o  16431  pwp1fsum  16439  divalglem2  16443  divalglem9  16449  flodddiv4  16461  m1bits  16486  sadcp1  16501  sadeq  16518  smupp1  16526  smumul  16539  gcdaddmlem  16570  nn0expgcd  16611  3lcm2e6woprm  16662  nn0gcdsq  16799  phiprmpw  16823  prmdiv  16832  prmdiveq  16833  pythagtriplem1  16863  pythagtriplem12  16873  pythagtriplem14  16875  pockthi  16954  infpnlem1  16957  prmreclem4  16966  4sqlem12  17003  4sqlem13  17004  4sqlem19  17010  vdwapun  17021  vdwlem6  17033  0hashbc  17054  prmo2  17087  prmo3  17088  dec5dvds  17111  dec5nprm  17113  dec2nprm  17114  modxai  17115  modxp1i  17117  mod2xnegi  17118  modsubi  17119  gcdmodi  17121  decexp2  17122  decsplit0b  17127  decsplit1  17129  decsplit  17130  karatsuba  17131  2exp7  17135  2exp8  17136  3exp3  17139  5prm  17156  7prm  17158  11prm  17162  prmlem2  17167  37prm  17168  43prm  17169  83prm  17170  139prm  17171  163prm  17172  317prm  17173  631prm  17174  prmo5  17176  1259lem1  17178  1259lem2  17179  1259lem3  17180  1259lem4  17181  1259lem5  17182  2503lem1  17184  2503lem2  17185  2503lem3  17186  2503prm  17187  4001lem1  17188  4001lem2  17189  4001lem3  17190  4001lem4  17191  4001prm  17192  pwsbas  17547  rcaninv  17855  subsubc  17917  xpccatid  18257  subsubmgm  18748  subsubm  18851  smndex2dnrinv  18950  mulg2  19123  subsubg  19189  oppgmnd  19397  gsumwrev  19409  psgnunilem2  19537  sylow1lem1  19640  subgslw  19658  sylow3  19675  efginvrel2  19769  efgsfo  19781  frgpnabllem1  19915  gsumzaddlem  19963  gsummptfzsplitl  19975  gsummpt1n0  20007  dprdfid  20061  ablfac1lem  20112  pgpfac1lem3  20121  pgpfaclem1  20125  ablsimpgfindlem1  20151  mgpress  20176  mgpressOLD  20177  srgbinomlem4  20256  opprrng  20371  unitsubm  20412  subsubrng  20589  subsubrg  20626  cntzsdrg  20825  subdrgint  20826  lsslss  20982  xrsnsgrp  21443  gzrngunit  21474  expghm  21509  pzriprng1ALT  21530  chrid  21563  zrhpsgnmhm  21625  psgndiflemA  21642  frlmip  21821  frlmphl  21824  evlsval  22133  mpff  22151  coe1fzgsumdlem  22328  evl1gsumdlem  22381  matvsca2  22455  mattposvs  22482  m2detleiblem3  22656  m2detleiblem4  22657  cpmidpmat  22900  resstopn  23215  cnmpt1res  23705  ressuss  24292  iscusp2  24332  ucnextcn  24334  txmetcnp  24581  rerest  24845  xrtgioo  24847  xrrest  24848  cnmpopc  24974  xrhmeo  24996  clmvs2  25146  clmnegneg  25156  ncvsm1  25207  ncvspi  25209  cphassir  25268  cphipval2  25294  reust  25434  rrxprds  25442  csbren  25452  rrxdsfi  25464  minveclem2  25479  ovolunlem1a  25550  ovolicc2lem4  25574  uniioombllem5  25641  iblabs  25884  iblabsr  25885  iblmulc2  25886  itgmulc2  25889  limcres  25941  dvfval  25952  dvreslem  25964  dvres2lem  25965  dvcnp2  25975  dvcnp2OLD  25976  cpnres  25993  dvmulbr  25995  dvcobr  26003  dvcobrOLD  26004  dveflem  26037  lhop1lem  26072  lhop2  26074  dvcnvrelem2  26077  plyun0  26256  coeeulem  26283  coeeu  26284  dvply1  26343  dvtaylp  26430  taylthlem2  26434  taylthlem2OLD  26435  taylth  26436  dvradcnv  26482  pserdvlem2  26490  abelthlem8  26501  abelth  26503  sinhalfpilem  26523  cospi  26532  eulerid  26534  cos2pi  26536  ef2kpi  26538  sinhalfpip  26552  sinhalfpim  26553  coshalfpip  26554  coshalfpim  26555  sincosq3sgn  26560  sincosq4sgn  26561  tangtx  26565  sincos4thpi  26573  sincos6thpi  26576  sineq0  26584  tanregt0  26599  logm1  26649  abslogle  26678  tanarg  26679  logcnlem4  26705  advlogexp  26715  cxpsqrt  26763  dvsqrt  26802  dvcnsqrt  26804  cxpcn3  26809  root1cj  26817  cxpeq  26818  logb1  26830  2logb9irr  26856  sqrt2cxp2logb9e3  26860  ang180lem1  26870  ang180lem2  26871  ang180lem3  26872  lawcos  26877  isosctrlem1  26879  isosctrlem2  26880  quad2  26900  1cubrlem  26902  1cubr  26903  dcubic2  26905  mcubic  26908  binom4  26911  dquartlem1  26912  quart1lem  26916  quart1  26917  quartlem1  26918  asinlem  26929  asinlem2  26930  asinlem3a  26931  acosneg  26948  efiasin  26949  asinsinlem  26952  asinsin  26953  acoscos  26954  asin1  26955  acosbnd  26961  atancj  26971  efiatan  26973  atanlogaddlem  26974  efiatan2  26978  2efiatan  26979  tanatan  26980  cosatan  26982  atantan  26984  atanbndlem  26986  atans2  26992  dvatan  26996  atantayl  26998  atantayl2  26999  log2cnv  27005  log2tlbnd  27006  log2ublem2  27008  log2ublem3  27009  log2ub  27010  birthday  27015  jensenlem1  27048  amgmlem  27051  lgamgulmlem2  27091  lgamgulmlem5  27094  lgambdd  27098  ftalem2  27135  ftalem5  27138  ftalem6  27139  basellem2  27143  basellem3  27144  basellem5  27146  basellem8  27149  basellem9  27150  mule1  27209  ppi1i  27229  musum  27252  ppiublem1  27264  ppiub  27266  chtublem  27273  chtub  27274  dchrptlem1  27326  dchrptlem2  27327  bclbnd  27342  bposlem6  27351  bposlem8  27353  bposlem9  27354  lgsdir2lem1  27387  lgsdir2lem2  27388  lgsdir2lem4  27390  lgsdir2lem5  27391  lgsne0  27397  1lgs  27402  gausslemma2dlem0e  27422  gausslemma2dlem0f  27423  gausslemma2dlem3  27430  gausslemma2d  27436  lgseisenlem1  27437  lgseisenlem2  27438  lgseisenlem3  27439  lgseisenlem4  27440  lgseisen  27441  lgsquadlem1  27442  lgsquadlem2  27443  lgsquad2lem1  27446  lgsquad2lem2  27447  m1lgs  27450  2lgslem3a  27458  2lgslem3b  27459  2lgslem3c  27460  2lgslem3d  27461  2lgsoddprmlem3a  27472  2lgsoddprmlem3b  27473  2lgsoddprmlem3c  27474  2lgsoddprmlem3d  27475  addsqnreup  27505  chebbnd1lem2  27532  chebbnd1lem3  27533  rplogsumlem2  27547  dchrisum0flblem1  27570  dchrisum0re  27575  mulog2sumlem2  27597  chpdifbndlem1  27615  pntpbnd1a  27647  pntpbnd2  27649  pntibndlem2  27653  pntibndlem3  27654  pntlemg  27660  pntlemk  27668  pntlemo  27669  no2times  28419  zseo  28424  remulscllem1  28450  axsegconlem1  28950  ax5seglem7  28968  axlowdimlem3  28977  axlowdimlem16  28990  axlowdimlem17  28991  elntg2  29018  vdegp1bi  29573  vtxdginducedm1  29579  wlkp1lem1  29709  spthispth  29762  2wlkdlem1  29958  2pthd  29973  clwlkclwwlkfo  30041  3wlkdlem1  30191  3pthd  30206  eucrct2eupth  30277  numclwwlk5  30420  numclwwlk7  30423  frgrregord013  30427  ex-fl  30479  ex-mod  30481  ex-exp  30482  ex-bc  30484  ex-lcm  30490  ex-ind-dvds  30493  vc2OLD  30600  vc0  30606  vcm  30608  nvm1  30697  nvpi  30699  nvmtri  30703  nvge0  30705  ipval3  30741  ipidsq  30742  ip0i  30857  ip1ilem  30858  ip2i  30860  ipdirilem  30861  ipasslem10  30871  siilem1  30883  siii  30885  minvecolem2  30907  hvsubid  31058  hvaddsubval  31065  hvmul2negi  31080  hvadd12i  31089  hv2times  31093  hvnegdii  31094  hvaddcani  31097  hi01  31128  hisubcomi  31136  normlem0  31141  normlem1  31142  normlem3  31144  normlem9  31150  bcseqi  31152  normsqi  31164  norm-ii-i  31169  normsubi  31173  norm3difi  31179  norm3adifii  31180  normpar2i  31188  polid2i  31189  polidi  31190  chdmm2i  31510  chj12i  31554  spanunsni  31611  qlaxr5i  31667  osumcor2i  31676  spansnji  31678  pjadjii  31706  pjinormii  31708  pjsslem  31711  pjpythi  31754  mayete3i  31760  mayetes3i  31761  hoadd12i  31809  honegneg  31838  ho2times  31851  hoaddsubi  31853  hosd1i  31854  hosd2i  31855  honpncani  31859  lnopeq0lem1  32037  lnopunilem1  32042  lnophmlem2  32049  lnfn0i  32074  nmopcoadji  32133  nmopcoadj2i  32134  opsqrlem1  32172  opsqrlem5  32176  opsqrlem6  32177  pjclem3  32229  stadd3i  32280  mddmd2  32341  mdexchi  32367  cvexchlem  32400  atomli  32414  atordi  32416  atabs2i  32434  mdsymlem1  32435  iuninc  32583  suppss2f  32657  mptiffisupp  32705  suppss3  32738  dfdec100  32834  dpfrac1  32856  decdiv10  32860  dpmul100  32861  dp3mul10  32862  dpmul1000  32863  dpexpp1  32872  dpadd2  32874  dpadd  32875  dpmul  32877  dpmul4  32878  threehalves  32879  1mhdrd  32880  pfxlsw2ccat  32917  ccatws1f1olast  32919  chnub  32984  cyc2fv1  33114  cyc2fv2  33115  cycpmco2lem4  33122  cycpmco2lem5  33123  cyc3fv1  33130  cyc3fv2  33131  cyc3fv3  33132  archirngz  33169  gsumvsca2  33206  nn0omnd  33338  nn0archi  33340  xrge0slmod  33341  opprabs  33475  resssra  33602  lsssra  33603  fedgmullem1  33642  fedgmullem2  33643  fedgmul  33644  fldgenfldext  33678  algextdeglem1  33708  algextdeglem4  33711  constrrtcclem  33725  2sqr3minply  33738  lmatfvlem  33761  sqsscirc1  33854  cnvordtrestixx  33859  raddcn  33875  xrge0iifhom  33883  xrge0mulc1cn  33887  xrge0tmd  33891  lmlimxrge0  33894  qqhucn  33938  rrhcn  33943  qqtopn  33957  rrhqima  33960  brfae  34212  inelcarsg  34276  cndprobnul  34402  isrrvv  34408  ballotlem1  34451  ballotlem2  34453  ballotlemi1  34467  ballotlemii  34468  ballotlemic  34471  ballotlem1c  34472  ballotlemfrceq  34493  ballotth  34502  ofcs2  34522  signsvtn0  34547  signstfveq0  34554  signsvtp  34560  signsvtn  34561  signsvfpn  34562  signsvfnn  34563  signshf  34565  hashreprin  34597  reprfz1  34601  chtvalz  34606  breprexp  34610  breprexpnat  34611  hgt750lemd  34625  hgt750lem  34628  hgt750lem2  34629  subfacp1lem1  35147  subfacp1lem5  35152  subfacp1lem6  35153  subfaclim  35156  cvmliftlem5  35257  cvmliftlem8  35260  cvmliftlem10  35262  cvmliftlem13  35264  cvmlift2lem6  35276  cvmlift2lem12  35282  problem1  35633  problem2  35634  problem4  35636  quad3  35638  iexpire  35697  itgeq12i  36170  sin2h  37570  poimirlem16  37596  poimirlem17  37597  poimirlem18  37598  poimirlem19  37599  poimirlem20  37600  poimirlem21  37601  poimirlem22  37602  poimirlem26  37606  mblfinlem3  37619  ismblfin  37621  itg2addnclem3  37633  iblabsnc  37644  iblmulc2nc  37645  itgmulc2nc  37648  ftc1cnnc  37652  ftc1anclem6  37658  ftc1anclem7  37659  ftc1anclem8  37660  dvasin  37664  fdc  37705  heiborlem4  37774  heiborlem6  37776  dalem24  39654  pmod2iN  39806  cdleme9  40210  cdleme20aN  40266  cdleme22e  40301  cdleme22eALTN  40302  cdleme25cv  40315  cdleme29b  40332  cdlemh1  40772  cdlemh2  40773  cdlemk35  40869  cdlemkid1  40879  12gcd5e1  41960  60gcd7e1  41962  420gcd8e4  41963  12lcm5e60  41965  420lcm8e840  41968  lcm1un  41970  lcm2un  41971  lcm3un  41972  lcm4un  41973  lcm5un  41974  lcm6un  41975  lcm7un  41976  lcm8un  41977  3factsumint1  41978  3factsumint3  41980  lcmineqlem10  41995  3exp7  42010  3lexlogpow5ineq1  42011  3lexlogpow5ineq5  42017  aks4d1p1  42033  5bc2eq10  42099  2ap1caineq  42102  aks5lem3a  42146  aks5lem7  42157  sqmid3api  42272  sqn5i  42274  sqdeccom12  42278  235t711  42293  cxpi11d  42331  re1m1e0m0  42373  readdlid  42379  remul02  42381  sn-1ticom  42410  sn-mullid  42411  sn-0tie0  42415  sn-mul02  42416  sn-inelr  42443  mhphf2  42553  flt4lem5e  42611  sum9cubes  42627  pellexlem5  42789  reglog1  42852  jm2.23  42953  jm2.27c  42964  lnmlsslnm  43038  lmhmlnmsplit  43044  areaquad  43177  oaomoencom  43279  resqrtvalex  43607  imsqrtvalex  43608  cotrclrcl  43704  inductionexd  44117  hashnzfz2  44290  lhe4.4ex1a  44298  binomcxplemdvsum  44324  binomcxplemnotnn0  44325  binomcxp  44326  sineq0ALT  44908  unirnmapsn  45121  fzisoeu  45215  fsummulc1f  45492  fprodexp  45515  constlimc  45545  sumnnodd  45551  limcresiooub  45563  limcresioolb  45564  cncfshiftioo  45813  fperdvper  45840  dvnmul  45864  dvmptfprod  45866  itgsinexplem1  45875  stoweidlem11  45932  stoweidlem13  45934  stoweidlem26  45947  stoweidlem34  45955  wallispilem4  45989  wallispi2lem1  45992  wallispi2lem2  45993  stirlinglem11  46005  dirkerper  46017  dirkertrigeqlem1  46019  dirkertrigeqlem3  46021  dirkercncflem1  46024  dirkercncflem4  46027  fourierdlem30  46058  fourierdlem32  46060  fourierdlem33  46061  fourierdlem42  46070  fourierdlem46  46073  fourierdlem47  46074  fourierdlem57  46084  fourierdlem60  46087  fourierdlem61  46088  fourierdlem62  46089  fourierdlem68  46095  fourierdlem73  46100  fourierdlem79  46106  fourierdlem89  46116  fourierdlem90  46117  fourierdlem91  46118  fourierdlem96  46123  fourierdlem97  46124  fourierdlem98  46125  fourierdlem99  46126  fourierdlem100  46127  fourierdlem103  46130  fourierdlem104  46131  fourierdlem108  46135  fourierdlem110  46137  fourierdlem113  46140  sqwvfoura  46149  sqwvfourb  46150  fourierswlem  46151  fouriersw  46152  fouriercn  46153  etransclem4  46159  etransclem7  46162  etransclem23  46178  etransclem24  46179  etransclem25  46180  etransclem26  46181  etransclem31  46186  etransclem32  46187  etransclem35  46190  etransclem37  46192  etransclem46  46201  rrndistlt  46211  sge0tsms  46301  sge0xaddlem2  46355  vonioolem2  46602  natlocalincr  46795  upwordsing  46803  tworepnotupword  46805  1t10e1p1e11  47225  deccarry  47226  1fzopredsuc  47239  m1mod0mod1  47243  iccpartgt  47301  fmtno0  47414  fmtno1  47415  fmtnorec2  47417  fmtno2  47424  fmtno3  47425  fmtno4  47426  fmtno5  47431  257prm  47435  fmtnofac1  47444  fmtno4prmfac  47446  fmtno4prmfac193  47447  fmtno4nprmfac193  47448  m2prm  47465  m3prm  47466  flsqrt5  47468  3ndvds4  47469  139prmALT  47470  31prm  47471  127prm  47473  m11nprm  47475  lighneallem2  47480  lighneallem3  47481  3exp4mod41  47490  41prothprmlem1  47491  41prothprmlem2  47492  41prothprm  47493  m1expevenALTV  47521  1oddALTV  47564  6even  47585  8even  47587  2exp340mod341  47607  341fppr2  47608  4fppr1  47609  8exp8mod9  47610  9fppr8  47611  nfermltl8rev  47616  gbpart7  47641  gbpart9  47643  gbpart11  47644  sbgoldbo  47661  bgoldbtbndlem1  47679  tgoldbachlt  47690  altgsumbcALT  48078  lincfsuppcl  48142  linccl  48143  lincvalsn  48146  lincdifsn  48153  lincsum  48158  lincscm  48159  lindslinindimp2lem4  48190  lindslinindsimp2lem5  48191  snlindsntor  48200  lincresunit3lem2  48209  zlmodzxzldeplem3  48231  ldepsnlinc  48237  nn0sumshdiglemA  48353  nn0sumshdiglemB  48354  ackval2  48416  ackval2012  48425  ackval3012  48426  ackval41a  48428  ackval42  48430  ackval42a  48431  affinecomb1  48436  rrx2linest  48476  itschlc0yqe  48494  itsclc0yqsollem1  48496  itscnhlc0xyqsol  48499  itschlc0xyqsol1  48500  itsclquadb  48510  2itscplem2  48513  itscnhlinecirc02plem2  48517  sinh-conventional  48831  onetansqsecsq  48853  cotsqcscsq  48854  mvlraddi  48864  mvrladdi  48865  mvlrmuli  48871  amgmwlem  48896  amgmlemALT  48897