MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  oveq1i Structured version   Visualization version   GIF version

Theorem oveq1i 6700
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
StepHypRef Expression
1 oveq1i.1 . 2 𝐴 = 𝐵
2 oveq1 6697 . 2 (𝐴 = 𝐵 → (𝐴𝐹𝐶) = (𝐵𝐹𝐶))
31, 2ax-mp 5 1 (𝐴𝐹𝐶) = (𝐵𝐹𝐶)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1523  (class class class)co 6690
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-rex 2947  df-rab 2950  df-v 3233  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-sn 4211  df-pr 4213  df-op 4217  df-uni 4469  df-br 4686  df-iota 5889  df-fv 5934  df-ov 6693
This theorem is referenced by:  caov12  6904  caov411  6908  omopthlem1  7780  map1  8077  pw2eng  8107  fsuppunbi  8337  cnfcomlem  8634  cnfcom2  8637  infxpenc2  8883  adderpqlem  9814  addassnq  9818  distrnq  9821  halfnq  9836  archnq  9840  addclprlem2  9877  addcmpblnr  9928  ltsrpr  9936  m1m1sr  9952  recexsrlem  9962  sqgt0sr  9965  map2psrpr  9969  axi2m1  10018  axcnre  10023  mul02lem2  10251  addid1  10254  cnegex2  10256  addid2  10257  mvrraddi  10336  mvlladdi  10337  negsubdi  10375  mulneg1  10504  recextlem1  10695  recdiv  10769  divmul13i  10824  mvllmuli  10896  2p2e4  11182  2times  11183  3p2e5  11198  3p3e6  11199  4p2e6  11200  4p3e7  11201  4p4e8  11202  5p2e7  11203  5p3e8  11204  5p4e9  11205  5p5e10OLD  11206  6p2e8  11207  6p3e9  11208  6p4e10OLD  11209  7p2e9  11210  7p3e10OLD  11211  8p2e10OLD  11212  1mhlfehlf  11289  8th4div3  11290  halfpm6th  11291  nneo  11499  dfdecOLD  11533  9p1e10  11534  dfdec10  11535  num0h  11547  numsuc  11549  dec10p  11591  dec10pOLD  11592  numma  11595  nummac  11596  numma2c  11597  numadd  11598  numaddc  11599  nummul2c  11601  decaddci  11618  decsubi  11621  decsubiOLD  11622  decmul1  11623  decmul1OLD  11624  5p5e10  11634  6p4e10  11636  7p3e10  11641  8p2e10  11648  decbin0  11720  decbin2  11721  xmulm1  12149  xadddi2  12165  x2times  12167  elfzp1b  12455  elfzm1b  12456  fz1ssfz0  12474  fz0to4untppr  12481  fz0sn0fz1  12495  fz1fzo0m1  12555  fz0add1fz1  12577  elfz0lmr  12623  fldiv4p1lem1div2  12676  quoremz  12694  quoremnn0ALT  12696  uzrdgxfr  12806  mulexpz  12940  expaddz  12944  sqrecii  12986  sq4e2t8  13002  cu2  13003  i3  13006  iexpcyc  13009  binom2i  13014  binom3  13025  crreczi  13029  discr  13041  3dec  13090  sq10OLD  13091  3decOLD  13093  nn0opthlem1  13095  nn0opth2i  13098  faclbnd  13117  bcp1nk  13144  bcpasc  13148  hashp1i  13229  hashxplem  13258  hashpw  13261  hashfun  13262  hashbc  13275  ccatlid  13404  swrdccatin12  13537  revs1  13560  cats1cat  13652  cats2cat  13653  lsws2  13695  lsws3  13696  lsws4  13697  s3s4  13724  s2s5  13725  s5s2  13726  imre  13892  crim  13899  remullem  13912  cnpart  14024  sqrtneglem  14051  absexpz  14089  absimle  14093  sqreulem  14143  amgm2  14153  iseraltlem2  14457  iseraltlem3  14458  modfsummod  14570  binomlem  14605  binom11  14608  arisum  14636  arisum2  14637  georeclim  14647  geo2sum  14648  mertenslem1  14660  mertens  14662  prodfrec  14671  fprodm1s  14744  fprodp1s  14745  fprodmodd  14772  fallfacfwd  14811  0risefac  14813  bpolydiflem  14829  bpoly2  14832  bpoly3  14833  bpoly4  14834  fsumcube  14835  efzval  14876  resinval  14909  recosval  14910  efi4p  14911  tan0  14925  efival  14926  sinhval  14928  coshval  14929  cosadd  14939  cos2tsin  14953  ef01bndlem  14958  cos1bnd  14961  cos2bnd  14962  absefib  14972  efieq1re  14973  demoivreALT  14975  eirrlem  14976  rpnnen2lem3  14989  rpnnen2lem11  14997  ruclem7  15009  3dvds  15099  3dvdsOLD  15100  3dvdsdec  15101  3dvdsdecOLD  15102  3dvds2dec  15103  3dvds2decOLD  15104  odd2np1  15112  nn0o1gt2  15144  nn0o  15146  pwp1fsum  15161  divalglem2  15165  divalglem9  15171  flodddiv4  15184  m1bits  15209  sadcp1  15224  sadeq  15241  smupp1  15249  smumul  15262  gcdaddmlem  15292  3lcm2e6woprm  15375  nn0gcdsq  15507  phiprmpw  15528  prmdiv  15537  prmdiveq  15538  pythagtriplem1  15568  pythagtriplem12  15578  pythagtriplem14  15580  pockthi  15658  infpnlem1  15661  prmreclem4  15670  4sqlem12  15707  4sqlem13  15708  4sqlem19  15714  vdwapun  15725  vdwlem6  15737  0hashbc  15758  prmo2  15791  prmo3  15792  dec5dvds  15815  dec5nprm  15817  dec2nprm  15818  modxai  15819  modxp1i  15821  mod2xnegi  15822  modsubi  15823  gcdmodi  15825  decexp2  15826  decsplit0b  15831  decsplit1  15833  decsplit  15834  decsplit0bOLD  15835  decsplit1OLD  15837  decsplitOLD  15838  karatsuba  15839  karatsubaOLD  15840  2exp8  15843  3exp3  15845  5prm  15862  7prm  15864  11prm  15869  prmlem2  15874  37prm  15875  43prm  15876  83prm  15877  139prm  15878  163prm  15879  317prm  15880  631prm  15881  prmo5  15883  1259lem1  15885  1259lem2  15886  1259lem3  15887  1259lem4  15888  1259lem5  15889  1259prm  15890  2503lem1  15891  2503lem2  15892  2503lem3  15893  2503prm  15894  4001lem1  15895  4001lem2  15896  4001lem3  15897  4001lem4  15898  4001prm  15899  pwsbas  16194  rcaninv  16501  subsubc  16560  xpccatid  16875  subsubm  17404  mulg2  17597  subsubg  17664  oppgmnd  17830  gsumwrev  17842  psgnunilem2  17961  sylow1lem1  18059  subgslw  18077  sylow3  18094  efginvrel2  18186  efgsfo  18198  frgpnabllem1  18322  gsumzaddlem  18367  gsummptfzsplitl  18379  gsummpt1n0  18410  dprdfid  18462  ablfac1lem  18513  pgpfac1lem3  18522  pgpfaclem1  18526  mgpress  18546  srgbinomlem4  18589  opprring  18677  unitsubm  18716  subsubrg  18854  lsslss  19009  evlsval  19567  mpff  19581  coe1fzgsumdlem  19719  evl1gsumdlem  19768  xrsnsgrp  19830  gzrngunit  19860  expghm  19892  chrid  19923  zrhpsgnmhm  19978  psgndiflemA  19995  frlmip  20165  frlmphl  20168  matvsca2  20282  mattposvs  20309  m2detleiblem3  20483  m2detleiblem4  20484  cpmidpmat  20726  resstopn  21038  cnmpt1res  21527  ressuss  22114  iscusp2  22153  ucnextcn  22155  txmetcnp  22399  rerest  22654  xrtgioo  22656  xrrest  22657  cnmpt2pc  22774  xrhmeo  22792  clmvs2  22940  clmnegneg  22950  ncvsm1  23000  ncvspi  23002  cphassir  23061  cphipval2  23086  reust  23215  rrxprds  23223  csbren  23228  minveclem2  23243  ovolunlem1a  23310  ovolicc2lem4  23334  uniioombllem5  23401  iblabs  23640  iblabsr  23641  iblmulc2  23642  itgmulc2  23645  limcres  23695  dvfval  23706  dvreslem  23718  dvres2lem  23719  dvcnp2  23728  cpnres  23745  dvcobr  23754  dveflem  23787  lhop1lem  23821  lhop2  23823  dvcnvrelem2  23826  plyun0  23998  coeeulem  24025  coeeu  24026  dvply1  24084  dvtaylp  24169  taylthlem2  24173  taylth  24174  dvradcnv  24220  pserdvlem2  24227  abelthlem8  24238  abelth  24240  sinhalfpilem  24260  cospi  24269  eulerid  24271  cos2pi  24273  ef2kpi  24275  sinhalfpip  24289  sinhalfpim  24290  coshalfpip  24291  coshalfpim  24292  sincosq3sgn  24297  sincosq4sgn  24298  tangtx  24302  sincos4thpi  24310  sincos6thpi  24312  sineq0  24318  tanregt0  24330  logm1  24380  abslogle  24409  tanarg  24410  logcnlem4  24436  advlogexp  24446  cxpsqrt  24494  dvsqrt  24528  dvcnsqrt  24530  cxpcn3  24534  root1cj  24542  cxpeq  24543  logb1  24552  ang180lem1  24584  ang180lem2  24585  ang180lem3  24586  lawcos  24591  isosctrlem1  24593  isosctrlem2  24594  quad2  24611  1cubrlem  24613  1cubr  24614  dcubic1lem  24615  dcubic2  24616  mcubic  24619  binom4  24622  dquartlem1  24623  quart1lem  24627  quart1  24628  quartlem1  24629  asinlem  24640  asinlem2  24641  asinlem3a  24642  acosneg  24659  efiasin  24660  asinsinlem  24663  asinsin  24664  acoscos  24665  asin1  24666  acosbnd  24672  atancj  24682  efiatan  24684  atanlogaddlem  24685  efiatan2  24689  2efiatan  24690  tanatan  24691  cosatan  24693  atantan  24695  atanbndlem  24697  atans2  24703  dvatan  24707  atantayl  24709  atantayl2  24710  log2cnv  24716  log2tlbnd  24717  log2ublem2  24719  log2ublem3  24720  log2ub  24721  birthday  24726  jensenlem1  24758  amgmlem  24761  lgamgulmlem2  24801  lgamgulmlem5  24804  lgambdd  24808  ftalem2  24845  ftalem5  24848  ftalem6  24849  basellem2  24853  basellem3  24854  basellem5  24856  basellem8  24859  basellem9  24860  mule1  24919  ppi1i  24939  musum  24962  ppiublem1  24972  ppiublem2  24973  ppiub  24974  chtublem  24981  chtub  24982  dchrptlem1  25034  dchrptlem2  25035  bclbnd  25050  bposlem6  25059  bposlem8  25061  bposlem9  25062  lgsdir2lem1  25095  lgsdir2lem2  25096  lgsdir2lem4  25098  lgsdir2lem5  25099  lgsne0  25105  1lgs  25110  gausslemma2dlem0e  25130  gausslemma2dlem0f  25131  gausslemma2dlem3  25138  gausslemma2d  25144  lgseisenlem1  25145  lgseisenlem2  25146  lgseisenlem3  25147  lgseisenlem4  25148  lgseisen  25149  lgsquadlem1  25150  lgsquadlem2  25151  lgsquad2lem1  25154  lgsquad2lem2  25155  m1lgs  25158  2lgslem3a  25166  2lgslem3b  25167  2lgslem3c  25168  2lgslem3d  25169  2lgsoddprmlem3a  25180  2lgsoddprmlem3b  25181  2lgsoddprmlem3c  25182  2lgsoddprmlem3d  25183  chebbnd1lem2  25204  chebbnd1lem3  25205  rplogsumlem2  25219  dchrisum0flblem1  25242  dchrisum0re  25247  mulog2sumlem2  25269  chpdifbndlem1  25287  pntpbnd1a  25319  pntpbnd2  25321  pntibndlem2  25325  pntibndlem3  25326  pntlemg  25332  pntlemk  25340  pntlemo  25341  axsegconlem1  25842  ax5seglem7  25860  axlowdimlem3  25869  axlowdimlem16  25882  axlowdimlem17  25883  vdegp1bi  26489  vtxdginducedm1  26495  wlkp1lem1  26626  spthispth  26678  2wlkdlem1  26890  2pthd  26905  3wlkdlem1  27137  3pthd  27152  eucrct2eupth  27223  numclwwlk5  27375  numclwwlk7  27378  frgrregord013  27382  ex-fl  27434  ex-mod  27436  ex-exp  27437  ex-bc  27439  ex-lcm  27445  ex-ind-dvds  27448  vc2OLD  27551  vc0  27557  vcm  27559  nvm1  27648  nvpi  27650  nvmtri  27654  nvge0  27656  ipval3  27692  ipidsq  27693  ip0i  27808  ip1ilem  27809  ip2i  27811  ipdirilem  27812  ipasslem10  27822  siilem1  27834  siii  27836  minvecolem2  27859  hvsubid  28011  hvaddsubval  28018  hvmul2negi  28033  hvadd12i  28042  hv2times  28046  hvnegdii  28047  hvaddcani  28050  hi01  28081  hisubcomi  28089  normlem0  28094  normlem1  28095  normlem3  28097  normlem9  28103  bcseqi  28105  normsqi  28117  norm-ii-i  28122  normsubi  28126  norm3difi  28132  norm3adifii  28133  normpar2i  28141  polid2i  28142  polidi  28143  chdmm2i  28465  chj12i  28509  spanunsni  28566  qlaxr5i  28622  osumcor2i  28631  spansnji  28633  pjadjii  28661  pjinormii  28663  pjsslem  28666  pjpythi  28709  mayete3i  28715  mayetes3i  28716  hoadd12i  28764  honegneg  28793  ho2times  28806  hoaddsubi  28808  hosd1i  28809  hosd2i  28810  honpncani  28814  lnopeq0lem1  28992  lnopunilem1  28997  lnophmlem2  29004  lnfn0i  29029  nmopcoadji  29088  nmopcoadj2i  29089  opsqrlem1  29127  opsqrlem5  29131  opsqrlem6  29132  pjclem3  29184  stadd3i  29235  mddmd2  29296  mdexchi  29322  cvexchlem  29355  atomli  29369  atordi  29371  atabs2i  29389  mdsymlem1  29390  iuninc  29505  suppss2f  29567  suppss3  29630  dfdec100  29704  dpfrac1  29727  dpfrac1OLD  29728  decdiv10  29732  dpmul100  29733  dp3mul10  29734  dpmul1000  29735  dpexpp1  29744  dpadd2  29746  dpadd  29747  dpmul  29749  dpmul4  29750  threehalves  29751  1mhdrd  29752  archirngz  29871  gsumvsca2  29911  nn0omnd  29969  nn0archi  29971  xrge0slmod  29972  lmatfvlem  30009  sqsscirc1  30082  cnvordtrestixx  30087  raddcn  30103  xrge0iifhom  30111  xrge0mulc1cn  30115  xrge0tmd  30120  lmlimxrge0  30122  qqhucn  30164  rrhcn  30169  qqtopn  30183  rrhqima  30186  brfae  30439  inelcarsg  30501  cndprobnul  30627  isrrvv  30633  ballotlem1  30676  ballotlem2  30678  ballotlemi1  30692  ballotlemii  30693  ballotlemic  30696  ballotlem1c  30697  ballotlemfrceq  30718  ballotth  30727  ofcs2  30750  signsvtn0  30775  signstfveq0  30782  signsvtp  30788  signsvtn  30789  signsvfpn  30790  signsvfnn  30791  signshf  30793  hashreprin  30826  reprfz1  30830  chtvalz  30835  breprexp  30839  breprexpnat  30840  hgt750lemd  30854  hgt750lem  30857  hgt750lem2  30858  subfacp1lem1  31287  subfacp1lem5  31292  subfacp1lem6  31293  subfaclim  31296  cvmliftlem5  31397  cvmliftlem8  31400  cvmliftlem10  31402  cvmliftlem13  31404  cvmlift2lem6  31416  cvmlift2lem12  31422  problem1  31684  problem2  31685  problem2OLD  31686  problem4  31688  quad3  31690  iexpire  31747  sin2h  33529  poimirlem16  33555  poimirlem17  33556  poimirlem18  33557  poimirlem19  33558  poimirlem20  33559  poimirlem21  33560  poimirlem22  33561  poimirlem26  33565  mblfinlem3  33578  ismblfin  33580  itg2addnclem3  33593  iblabsnc  33604  iblmulc2nc  33605  itgmulc2nc  33608  ftc1cnnc  33614  ftc1anclem6  33620  ftc1anclem7  33621  ftc1anclem8  33622  dvasin  33626  fdc  33671  heiborlem4  33743  heiborlem6  33745  dalem24  35301  pmod2iN  35453  cdleme9  35858  cdleme20aN  35914  cdleme22e  35949  cdleme22eALTN  35950  cdleme25cv  35963  cdleme29b  35980  cdlemh1  36420  cdlemh2  36421  cdlemk35  36517  cdlemkid1  36527  pellexlem5  37714  reglog1  37777  jm2.23  37880  jm2.27c  37891  lnmlsslnm  37968  lmhmlnmsplit  37974  cntzsdrg  38089  areaquad  38119  cotrclrcl  38351  inductionexd  38770  hashnzfz2  38837  lhe4.4ex1a  38845  binomcxplemdvsum  38871  binomcxplemnotnn0  38872  binomcxp  38873  sineq0ALT  39487  unirnmapsn  39720  fzisoeu  39828  fsummulc1f  40120  fprodexp  40144  constlimc  40174  sumnnodd  40180  limcresiooub  40192  limcresioolb  40193  cncfshiftioo  40423  fperdvper  40451  dvnmul  40476  dvmptfprod  40478  itgsinexplem1  40487  stoweidlem11  40546  stoweidlem13  40548  stoweidlem26  40561  stoweidlem34  40569  wallispilem4  40603  wallispi2lem1  40606  wallispi2lem2  40607  stirlinglem11  40619  dirkerper  40631  dirkertrigeqlem1  40633  dirkertrigeqlem3  40635  dirkercncflem1  40638  dirkercncflem4  40641  fourierdlem30  40672  fourierdlem32  40674  fourierdlem33  40675  fourierdlem42  40684  fourierdlem46  40687  fourierdlem47  40688  fourierdlem57  40698  fourierdlem60  40701  fourierdlem61  40702  fourierdlem62  40703  fourierdlem68  40709  fourierdlem73  40714  fourierdlem79  40720  fourierdlem89  40730  fourierdlem90  40731  fourierdlem91  40732  fourierdlem96  40737  fourierdlem97  40738  fourierdlem98  40739  fourierdlem99  40740  fourierdlem100  40741  fourierdlem103  40744  fourierdlem104  40745  fourierdlem108  40749  fourierdlem110  40751  fourierdlem113  40754  sqwvfoura  40763  sqwvfourb  40764  fourierswlem  40765  fouriersw  40766  fouriercn  40767  etransclem4  40773  etransclem7  40776  etransclem23  40792  etransclem24  40793  etransclem25  40794  etransclem26  40795  etransclem31  40800  etransclem32  40801  etransclem35  40804  etransclem37  40806  etransclem46  40815  rrxdsfi  40823  rrndistlt  40828  sge0tsms  40915  sge0xaddlem2  40969  vonioolem2  41216  1t10e1p1e11  41644  1t10e1p1e11OLD  41645  deccarry  41646  1fzopredsuc  41659  m1mod0mod1  41664  iccpartgt  41688  pfxccatin12  41750  fmtno0  41777  fmtno1  41778  fmtnorec2  41780  fmtno2  41787  fmtno3  41788  fmtno4  41789  fmtno5  41794  257prm  41798  fmtnofac1  41807  fmtno4prmfac  41809  fmtno4prmfac193  41810  fmtno4nprmfac193  41811  pwdif  41826  m2prm  41830  m3prm  41831  flsqrt5  41834  3ndvds4  41835  139prmALT  41836  31prm  41837  2exp7  41839  127prm  41840  m11nprm  41843  lighneallem2  41848  lighneallem3  41849  3exp4mod41  41858  41prothprmlem1  41859  41prothprmlem2  41860  41prothprm  41861  m1expevenALTV  41885  1oddALTV  41926  6even  41945  8even  41947  gbpart7  41980  gbpart9  41982  gbpart11  41983  sbgoldbo  42000  bgoldbtbndlem1  42018  tgoldbachlt  42029  tgoldbachltOLD  42035  subsubmgm  42122  altgsumbcALT  42456  lincfsuppcl  42527  linccl  42528  lincvalsn  42531  lincdifsn  42538  lincsum  42543  lincscm  42544  lindslinindimp2lem4  42575  lindslinindsimp2lem5  42576  snlindsntor  42585  lincresunit3lem2  42594  zlmodzxzldeplem3  42616  ldepsnlinc  42622  nn0sumshdiglemA  42738  nn0sumshdiglemB  42739  sinh-conventional  42808  onetansqsecsq  42830  cotsqcscsq  42831  mvlraddi  42842  mvrladdi  42844  mvlrmuli  42851  amgmwlem  42876  amgmlemALT  42877
  Copyright terms: Public domain W3C validator