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

Theorem oveq1i 6880
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 6877 . 2 (𝐴 = 𝐵 → (𝐴𝐹𝐶) = (𝐵𝐹𝐶))
31, 2ax-mp 5 1 (𝐴𝐹𝐶) = (𝐵𝐹𝐶)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1637  (class class class)co 6870
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-rex 3102  df-rab 3105  df-v 3393  df-dif 3772  df-un 3774  df-in 3776  df-ss 3783  df-nul 4117  df-if 4280  df-sn 4371  df-pr 4373  df-op 4377  df-uni 4631  df-br 4845  df-iota 6060  df-fv 6105  df-ov 6873
This theorem is referenced by:  caov12  7088  caov411  7092  omopthlem1  7968  map1  8271  pw2eng  8301  fsuppunbi  8531  cnfcomlem  8839  cnfcom2  8842  infxpenc2  9124  adderpqlem  10057  addassnq  10061  distrnq  10064  halfnq  10079  archnq  10083  addclprlem2  10120  addcmpblnr  10171  ltsrpr  10179  m1m1sr  10195  recexsrlem  10205  sqgt0sr  10208  map2psrpr  10212  axi2m1  10261  axcnre  10266  mul02lem2  10494  addid1  10497  cnegex2  10499  addid2  10500  mvrraddi  10579  mvlladdi  10580  negsubdi  10618  mulneg1  10747  recextlem1  10938  recdiv  11012  divmul13i  11067  mvllmuli  11139  2p2e4  11423  2times  11424  3p2e5  11438  3p3e6  11439  4p2e6  11440  4p3e7  11441  4p4e8  11442  5p2e7  11443  5p3e8  11444  5p4e9  11445  6p2e8  11446  6p3e9  11447  7p2e9  11448  1mhlfehlf  11514  8th4div3  11515  halfpm6th  11516  nneo  11723  9p1e10  11757  dfdec10  11758  num0h  11767  numsuc  11769  dec10p  11798  numma  11799  nummac  11800  numma2c  11801  numadd  11802  numaddc  11803  nummul2c  11805  decaddci  11816  decsubi  11818  decmul1  11819  5p5e10  11826  6p4e10  11827  7p3e10  11830  8p2e10  11835  decbin0  11895  decbin2  11896  xmulm1  12325  xadddi2  12341  x2times  12343  elfzp1b  12636  elfzm1b  12637  fz1ssfz0  12655  fz0to4untppr  12662  fz0sn0fz1  12676  fz1fzo0m1  12736  fz0add1fz1  12758  elfz0lmr  12803  fldiv4p1lem1div2  12856  quoremz  12874  quoremnn0ALT  12876  uzrdgxfr  12986  mulexpz  13119  expaddz  13123  sqrecii  13165  sq4e2t8  13181  cu2  13182  i3  13185  iexpcyc  13188  binom2i  13193  binom3  13204  crreczi  13208  discr  13220  3dec  13269  nn0opthlem1  13271  nn0opth2i  13274  faclbnd  13293  bcp1nk  13320  bcpasc  13324  hashp1i  13404  hashxplem  13433  hashpw  13436  hashfun  13437  hashbc  13450  ccatlid  13579  swrdccatin12  13711  revs1  13734  cats1cat  13826  cats2cat  13827  lsws2  13869  lsws3  13870  lsws4  13871  s3s4  13898  s2s5  13899  s5s2  13900  imre  14067  crim  14074  remullem  14087  cnpart  14199  sqrtneglem  14226  absexpz  14264  absimle  14268  sqreulem  14318  amgm2  14328  iseraltlem2  14632  iseraltlem3  14633  modfsummod  14744  binomlem  14779  binom11  14782  arisum  14810  arisum2  14811  georeclim  14821  geo2sum  14822  mertenslem1  14833  mertens  14835  prodfrec  14844  fprodm1s  14917  fprodp1s  14918  fprodmodd  14944  fallfacfwd  14983  0risefac  14985  bpolydiflem  15001  bpoly2  15004  bpoly3  15005  bpoly4  15006  fsumcube  15007  efzval  15048  resinval  15081  recosval  15082  efi4p  15083  tan0  15097  efival  15098  sinhval  15100  coshval  15101  cosadd  15111  cos2tsin  15125  ef01bndlem  15130  cos1bnd  15133  cos2bnd  15134  absefib  15144  efieq1re  15145  demoivreALT  15147  eirrlem  15148  rpnnen2lem3  15161  rpnnen2lem11  15169  ruclem7  15181  3dvds  15271  3dvdsdec  15272  3dvds2dec  15273  odd2np1  15281  nn0o1gt2  15313  nn0o  15315  pwp1fsum  15330  divalglem2  15334  divalglem9  15340  flodddiv4  15352  m1bits  15377  sadcp1  15392  sadeq  15409  smupp1  15417  smumul  15430  gcdaddmlem  15460  3lcm2e6woprm  15543  nn0gcdsq  15673  phiprmpw  15694  prmdiv  15703  prmdiveq  15704  pythagtriplem1  15734  pythagtriplem12  15744  pythagtriplem14  15746  pockthi  15824  infpnlem1  15827  prmreclem4  15836  4sqlem12  15873  4sqlem13  15874  4sqlem19  15880  vdwapun  15891  vdwlem6  15903  0hashbc  15924  prmo2  15957  prmo3  15958  dec5dvds  15981  dec5nprm  15983  dec2nprm  15984  modxai  15985  modxp1i  15987  mod2xnegi  15988  modsubi  15989  gcdmodi  15991  decexp2  15992  decsplit0b  15997  decsplit1  15999  decsplit  16000  karatsuba  16001  2exp8  16004  3exp3  16006  5prm  16023  7prm  16025  11prm  16029  prmlem2  16034  37prm  16035  43prm  16036  83prm  16037  139prm  16038  163prm  16039  317prm  16040  631prm  16041  prmo5  16043  1259lem1  16045  1259lem2  16046  1259lem3  16047  1259lem4  16048  1259lem5  16049  1259prm  16050  2503lem1  16051  2503lem2  16052  2503lem3  16053  2503prm  16054  4001lem1  16055  4001lem2  16056  4001lem3  16057  4001lem4  16058  4001prm  16059  pwsbas  16348  rcaninv  16654  subsubc  16713  xpccatid  17029  subsubm  17558  mulg2  17751  subsubg  17815  oppgmnd  17981  gsumwrev  17993  psgnunilem2  18112  sylow1lem1  18210  subgslw  18228  sylow3  18245  efginvrel2  18337  efgsfo  18349  frgpnabllem1  18473  gsumzaddlem  18518  gsummptfzsplitl  18530  gsummpt1n0  18561  dprdfid  18614  ablfac1lem  18665  pgpfac1lem3  18674  pgpfaclem1  18678  mgpress  18698  srgbinomlem4  18741  opprring  18829  unitsubm  18868  subsubrg  19006  lsslss  19164  evlsval  19723  mpff  19737  coe1fzgsumdlem  19875  evl1gsumdlem  19924  xrsnsgrp  19986  gzrngunit  20016  expghm  20048  chrid  20079  zrhpsgnmhm  20133  psgndiflemA  20151  frlmip  20323  frlmphl  20326  matvsca2  20440  mattposvs  20468  m2detleiblem3  20642  m2detleiblem4  20643  cpmidpmat  20887  resstopn  21200  cnmpt1res  21689  ressuss  22276  iscusp2  22315  ucnextcn  22317  txmetcnp  22561  rerest  22816  xrtgioo  22818  xrrest  22819  cnmpt2pc  22936  xrhmeo  22954  clmvs2  23102  clmnegneg  23112  ncvsm1  23162  ncvspi  23164  cphassir  23223  cphipval2  23248  reust  23377  rrxprds  23385  csbren  23390  minveclem2  23405  ovolunlem1a  23473  ovolicc2lem4  23497  uniioombllem5  23564  iblabs  23805  iblabsr  23806  iblmulc2  23807  itgmulc2  23810  limcres  23860  dvfval  23871  dvreslem  23883  dvres2lem  23884  dvcnp2  23893  cpnres  23910  dvcobr  23919  dveflem  23952  lhop1lem  23986  lhop2  23988  dvcnvrelem2  23991  plyun0  24163  coeeulem  24190  coeeu  24191  dvply1  24249  dvtaylp  24334  taylthlem2  24338  taylth  24339  dvradcnv  24385  pserdvlem2  24392  abelthlem8  24403  abelth  24405  sinhalfpilem  24426  cospi  24435  eulerid  24437  cos2pi  24439  ef2kpi  24441  sinhalfpip  24455  sinhalfpim  24456  coshalfpip  24457  coshalfpim  24458  sincosq3sgn  24463  sincosq4sgn  24464  tangtx  24468  sincos4thpi  24476  sincos6thpi  24478  sineq0  24484  tanregt0  24496  logm1  24545  abslogle  24574  tanarg  24575  logcnlem4  24601  advlogexp  24611  cxpsqrt  24659  dvsqrt  24693  dvcnsqrt  24695  cxpcn3  24699  root1cj  24707  cxpeq  24708  logb1  24717  ang180lem1  24749  ang180lem2  24750  ang180lem3  24751  lawcos  24756  isosctrlem1  24758  isosctrlem2  24759  quad2  24776  1cubrlem  24778  1cubr  24779  dcubic1lem  24780  dcubic2  24781  mcubic  24784  binom4  24787  dquartlem1  24788  quart1lem  24792  quart1  24793  quartlem1  24794  asinlem  24805  asinlem2  24806  asinlem3a  24807  acosneg  24824  efiasin  24825  asinsinlem  24828  asinsin  24829  acoscos  24830  asin1  24831  acosbnd  24837  atancj  24847  efiatan  24849  atanlogaddlem  24850  efiatan2  24854  2efiatan  24855  tanatan  24856  cosatan  24858  atantan  24860  atanbndlem  24862  atans2  24868  dvatan  24872  atantayl  24874  atantayl2  24875  log2cnv  24881  log2tlbnd  24882  log2ublem2  24884  log2ublem3  24885  log2ub  24886  birthday  24891  jensenlem1  24923  amgmlem  24926  lgamgulmlem2  24966  lgamgulmlem5  24969  lgambdd  24973  ftalem2  25010  ftalem5  25013  ftalem6  25014  basellem2  25018  basellem3  25019  basellem5  25021  basellem8  25024  basellem9  25025  mule1  25084  ppi1i  25104  musum  25127  ppiublem1  25137  ppiublem2  25138  ppiub  25139  chtublem  25146  chtub  25147  dchrptlem1  25199  dchrptlem2  25200  bclbnd  25215  bposlem6  25224  bposlem8  25226  bposlem9  25227  lgsdir2lem1  25260  lgsdir2lem2  25261  lgsdir2lem4  25263  lgsdir2lem5  25264  lgsne0  25270  1lgs  25275  gausslemma2dlem0e  25295  gausslemma2dlem0f  25296  gausslemma2dlem3  25303  gausslemma2d  25309  lgseisenlem1  25310  lgseisenlem2  25311  lgseisenlem3  25312  lgseisenlem4  25313  lgseisen  25314  lgsquadlem1  25315  lgsquadlem2  25316  lgsquad2lem1  25319  lgsquad2lem2  25320  m1lgs  25323  2lgslem3a  25331  2lgslem3b  25332  2lgslem3c  25333  2lgslem3d  25334  2lgsoddprmlem3a  25345  2lgsoddprmlem3b  25346  2lgsoddprmlem3c  25347  2lgsoddprmlem3d  25348  chebbnd1lem2  25369  chebbnd1lem3  25370  rplogsumlem2  25384  dchrisum0flblem1  25407  dchrisum0re  25412  mulog2sumlem2  25434  chpdifbndlem1  25452  pntpbnd1a  25484  pntpbnd2  25486  pntibndlem2  25490  pntibndlem3  25491  pntlemg  25497  pntlemk  25505  pntlemo  25506  axsegconlem1  26007  ax5seglem7  26025  axlowdimlem3  26034  axlowdimlem16  26047  axlowdimlem17  26048  vdegp1bi  26657  vtxdginducedm1  26663  wlkp1lem1  26794  spthispth  26846  2wlkdlem1  27061  2pthd  27076  clwlkclwwlkfo  27148  3wlkdlem1  27328  3pthd  27343  eucrct2eupth  27414  numclwwlk5  27572  numclwwlk7  27575  frgrregord013  27579  ex-fl  27631  ex-mod  27633  ex-exp  27634  ex-bc  27636  ex-lcm  27642  ex-ind-dvds  27645  vc2OLD  27747  vc0  27753  vcm  27755  nvm1  27844  nvpi  27846  nvmtri  27850  nvge0  27852  ipval3  27888  ipidsq  27889  ip0i  28004  ip1ilem  28005  ip2i  28007  ipdirilem  28008  ipasslem10  28018  siilem1  28030  siii  28032  minvecolem2  28055  hvsubid  28207  hvaddsubval  28214  hvmul2negi  28229  hvadd12i  28238  hv2times  28242  hvnegdii  28243  hvaddcani  28246  hi01  28277  hisubcomi  28285  normlem0  28290  normlem1  28291  normlem3  28293  normlem9  28299  bcseqi  28301  normsqi  28313  norm-ii-i  28318  normsubi  28322  norm3difi  28328  norm3adifii  28329  normpar2i  28337  polid2i  28338  polidi  28339  chdmm2i  28661  chj12i  28705  spanunsni  28762  qlaxr5i  28818  osumcor2i  28827  spansnji  28829  pjadjii  28857  pjinormii  28859  pjsslem  28862  pjpythi  28905  mayete3i  28911  mayetes3i  28912  hoadd12i  28960  honegneg  28989  ho2times  29002  hoaddsubi  29004  hosd1i  29005  hosd2i  29006  honpncani  29010  lnopeq0lem1  29188  lnopunilem1  29193  lnophmlem2  29200  lnfn0i  29225  nmopcoadji  29284  nmopcoadj2i  29285  opsqrlem1  29323  opsqrlem5  29327  opsqrlem6  29328  pjclem3  29380  stadd3i  29431  mddmd2  29492  mdexchi  29518  cvexchlem  29551  atomli  29565  atordi  29567  atabs2i  29585  mdsymlem1  29586  iuninc  29700  suppss2f  29762  suppss3  29825  dfdec100  29899  dpfrac1  29921  decdiv10  29925  dpmul100  29926  dp3mul10  29927  dpmul1000  29928  dpexpp1  29937  dpadd2  29939  dpadd  29940  dpmul  29942  dpmul4  29943  threehalves  29944  1mhdrd  29945  archirngz  30064  gsumvsca2  30104  nn0omnd  30162  nn0archi  30164  xrge0slmod  30165  lmatfvlem  30202  sqsscirc1  30275  cnvordtrestixx  30280  raddcn  30296  xrge0iifhom  30304  xrge0mulc1cn  30308  xrge0tmd  30313  lmlimxrge0  30315  qqhucn  30357  rrhcn  30362  qqtopn  30376  rrhqima  30379  brfae  30632  inelcarsg  30694  cndprobnul  30820  isrrvv  30826  ballotlem1  30869  ballotlem2  30871  ballotlemi1  30885  ballotlemii  30886  ballotlemic  30889  ballotlem1c  30890  ballotlemfrceq  30911  ballotth  30920  ofcs2  30943  signsvtn0  30968  signstfveq0  30975  signsvtp  30981  signsvtn  30982  signsvfpn  30983  signsvfnn  30984  signshf  30986  hashreprin  31019  reprfz1  31023  chtvalz  31028  breprexp  31032  breprexpnat  31033  hgt750lemd  31047  hgt750lem  31050  hgt750lem2  31051  subfacp1lem1  31479  subfacp1lem5  31484  subfacp1lem6  31485  subfaclim  31488  cvmliftlem5  31589  cvmliftlem8  31592  cvmliftlem10  31594  cvmliftlem13  31596  cvmlift2lem6  31608  cvmlift2lem12  31614  problem1  31876  problem2  31877  problem4  31879  quad3  31881  iexpire  31938  sin2h  33707  poimirlem16  33733  poimirlem17  33734  poimirlem18  33735  poimirlem19  33736  poimirlem20  33737  poimirlem21  33738  poimirlem22  33739  poimirlem26  33743  mblfinlem3  33756  ismblfin  33758  itg2addnclem3  33770  iblabsnc  33781  iblmulc2nc  33782  itgmulc2nc  33785  ftc1cnnc  33791  ftc1anclem6  33797  ftc1anclem7  33798  ftc1anclem8  33799  dvasin  33803  fdc  33847  heiborlem4  33919  heiborlem6  33921  dalem24  35472  pmod2iN  35624  cdleme9  36028  cdleme20aN  36084  cdleme22e  36119  cdleme22eALTN  36120  cdleme25cv  36133  cdleme29b  36150  cdlemh1  36590  cdlemh2  36591  cdlemk35  36687  cdlemkid1  36697  sqmid3api  37739  sqn5i  37740  pellexlem5  37893  reglog1  37956  jm2.23  38058  jm2.27c  38069  lnmlsslnm  38146  lmhmlnmsplit  38152  cntzsdrg  38267  areaquad  38296  cotrclrcl  38528  inductionexd  38947  hashnzfz2  39014  lhe4.4ex1a  39022  binomcxplemdvsum  39048  binomcxplemnotnn0  39049  binomcxp  39050  sineq0ALT  39661  unirnmapsn  39887  fzisoeu  39989  fsummulc1f  40276  fprodexp  40300  constlimc  40330  sumnnodd  40336  limcresiooub  40348  limcresioolb  40349  cncfshiftioo  40579  fperdvper  40607  dvnmul  40632  dvmptfprod  40634  itgsinexplem1  40643  stoweidlem11  40701  stoweidlem13  40703  stoweidlem26  40716  stoweidlem34  40724  wallispilem4  40758  wallispi2lem1  40761  wallispi2lem2  40762  stirlinglem11  40774  dirkerper  40786  dirkertrigeqlem1  40788  dirkertrigeqlem3  40790  dirkercncflem1  40793  dirkercncflem4  40796  fourierdlem30  40827  fourierdlem32  40829  fourierdlem33  40830  fourierdlem42  40839  fourierdlem46  40842  fourierdlem47  40843  fourierdlem57  40853  fourierdlem60  40856  fourierdlem61  40857  fourierdlem62  40858  fourierdlem68  40864  fourierdlem73  40869  fourierdlem79  40875  fourierdlem89  40885  fourierdlem90  40886  fourierdlem91  40887  fourierdlem96  40892  fourierdlem97  40893  fourierdlem98  40894  fourierdlem99  40895  fourierdlem100  40896  fourierdlem103  40899  fourierdlem104  40900  fourierdlem108  40904  fourierdlem110  40906  fourierdlem113  40909  sqwvfoura  40918  sqwvfourb  40919  fourierswlem  40920  fouriersw  40921  fouriercn  40922  etransclem4  40928  etransclem7  40931  etransclem23  40947  etransclem24  40948  etransclem25  40949  etransclem26  40950  etransclem31  40955  etransclem32  40956  etransclem35  40959  etransclem37  40961  etransclem46  40970  rrxdsfi  40978  rrndistlt  40983  sge0tsms  41070  sge0xaddlem2  41124  vonioolem2  41371  1t10e1p1e11  41889  deccarry  41890  1fzopredsuc  41903  m1mod0mod1  41908  iccpartgt  41932  pfxccatin12  41994  fmtno0  42021  fmtno1  42022  fmtnorec2  42024  fmtno2  42031  fmtno3  42032  fmtno4  42033  fmtno5  42038  257prm  42042  fmtnofac1  42051  fmtno4prmfac  42053  fmtno4prmfac193  42054  fmtno4nprmfac193  42055  pwdif  42070  m2prm  42074  m3prm  42075  flsqrt5  42078  3ndvds4  42079  139prmALT  42080  31prm  42081  2exp7  42083  127prm  42084  m11nprm  42087  lighneallem2  42092  lighneallem3  42093  3exp4mod41  42102  41prothprmlem1  42103  41prothprmlem2  42104  41prothprm  42105  m1expevenALTV  42129  1oddALTV  42170  6even  42189  8even  42191  gbpart7  42224  gbpart9  42226  gbpart11  42227  sbgoldbo  42244  bgoldbtbndlem1  42262  tgoldbachlt  42273  subsubmgm  42359  altgsumbcALT  42693  lincfsuppcl  42764  linccl  42765  lincvalsn  42768  lincdifsn  42775  lincsum  42780  lincscm  42781  lindslinindimp2lem4  42812  lindslinindsimp2lem5  42813  snlindsntor  42822  lincresunit3lem2  42831  zlmodzxzldeplem3  42853  ldepsnlinc  42859  nn0sumshdiglemA  42975  nn0sumshdiglemB  42976  sinh-conventional  43045  onetansqsecsq  43067  cotsqcscsq  43068  mvlraddi  43079  mvrladdi  43081  mvlrmuli  43088  amgmwlem  43113  amgmlemALT  43114
  Copyright terms: Public domain W3C validator