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

Theorem oveq1i 7155
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 7152 . 2 (𝐴 = 𝐵 → (𝐴𝐹𝐶) = (𝐵𝐹𝐶))
31, 2ax-mp 5 1 (𝐴𝐹𝐶) = (𝐵𝐹𝐶)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1528  (class class class)co 7145
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2793
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rex 3144  df-rab 3147  df-v 3497  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-nul 4291  df-if 4466  df-sn 4560  df-pr 4562  df-op 4566  df-uni 4833  df-br 5059  df-iota 6308  df-fv 6357  df-ov 7148
This theorem is referenced by:  caov12  7365  caov411  7369  omopthlem1  8272  map1  8581  pw2eng  8612  fsuppunbi  8843  cnfcomlem  9151  cnfcom2  9154  infxpenc2  9437  adderpqlem  10365  addassnq  10369  distrnq  10372  halfnq  10387  archnq  10391  addclprlem2  10428  addcmpblnr  10480  ltsrpr  10488  m1m1sr  10504  recexsrlem  10514  sqgt0sr  10517  map2psrpr  10521  axi2m1  10570  axcnre  10575  mul02lem2  10806  addid1  10809  cnegex2  10811  addid2  10812  mvrraddi  10892  mvlladdi  10893  negsubdi  10931  mulneg1  11065  recextlem1  11259  recdiv  11335  divmul13i  11390  mvllmuli  11462  2p2e4  11761  2times  11762  1p2e3  11769  3p2e5  11777  3p3e6  11778  4p2e6  11779  4p3e7  11780  4p4e8  11781  5p2e7  11782  5p3e8  11783  5p4e9  11784  6p2e8  11785  6p3e9  11786  7p2e9  11787  1mhlfehlf  11845  8th4div3  11846  halfpm6th  11847  nneo  12055  9p1e10  12089  dfdec10  12090  num0h  12099  numsuc  12101  dec10p  12130  numma  12131  nummac  12132  numma2c  12133  numadd  12134  numaddc  12135  nummul2c  12137  decaddci  12148  decsubi  12150  5p5e10  12158  6p4e10  12159  7p3e10  12162  8p2e10  12167  decbin0  12227  decbin2  12228  xmulm1  12664  xadddi2  12680  x2times  12682  elfzp1b  12974  elfzm1b  12975  fz1ssfz0  12993  fz0to4untppr  13000  fz0sn0fz1  13014  fz0add1fz1  13097  elfz0lmr  13142  fldiv4p1lem1div2  13195  quoremz  13213  quoremnn0ALT  13215  uzrdgxfr  13325  mulexpz  13459  expaddz  13463  sqrecii  13536  sq4e2t8  13552  cu2  13553  i3  13556  iexpcyc  13559  binom2i  13564  binom3  13575  crreczi  13579  discr  13591  3dec  13616  nn0opthlem1  13618  nn0opth2i  13621  faclbnd  13640  bcp1nk  13667  bcpasc  13671  hashp1i  13754  hashxplem  13784  hashpw  13787  hashfun  13788  hashbc  13801  ccatlid  13930  pfxccatin12lem2c  14082  revs1  14117  cats1cat  14213  cats2cat  14214  lsws2  14256  lsws3  14257  lsws4  14258  s3s4  14285  s2s5  14286  s5s2  14287  imre  14457  crim  14464  remullem  14477  cnpart  14589  sqrtneglem  14616  absexpz  14655  absimle  14659  sqreulem  14709  amgm2  14719  iseraltlem2  15029  iseraltlem3  15030  modfsummod  15139  binomlem  15174  binom11  15177  arisum  15205  arisum2  15206  pwdif  15213  georeclim  15218  geo2sum  15219  mertenslem1  15230  mertens  15232  prodfrec  15241  fprodm1s  15314  fprodp1s  15315  fprodmodd  15341  fallfacfwd  15380  0risefac  15382  bpolydiflem  15398  bpoly2  15401  bpoly3  15402  bpoly4  15403  fsumcube  15404  efzval  15445  resinval  15478  recosval  15479  efi4p  15480  tan0  15494  efival  15495  sinhval  15497  coshval  15498  cosadd  15508  cos2tsin  15522  ef01bndlem  15527  cos1bnd  15530  cos2bnd  15531  absefib  15541  efieq1re  15542  demoivreALT  15544  eirrlem  15547  rpnnen2lem3  15559  rpnnen2lem11  15567  ruclem7  15579  3dvds  15670  3dvdsdec  15671  3dvds2dec  15672  odd2np1  15680  nn0o1gt2  15722  nn0o  15724  pwp1fsum  15732  divalglem2  15736  divalglem9  15742  flodddiv4  15754  m1bits  15779  sadcp1  15794  sadeq  15811  smupp1  15819  smumul  15832  gcdaddmlem  15862  3lcm2e6woprm  15949  nn0gcdsq  16082  phiprmpw  16103  prmdiv  16112  prmdiveq  16113  pythagtriplem1  16143  pythagtriplem12  16153  pythagtriplem14  16155  pockthi  16233  infpnlem1  16236  prmreclem4  16245  4sqlem12  16282  4sqlem13  16283  4sqlem19  16289  vdwapun  16300  vdwlem6  16312  0hashbc  16333  prmo2  16366  prmo3  16367  dec5dvds  16390  dec5nprm  16392  dec2nprm  16393  modxai  16394  modxp1i  16396  mod2xnegi  16397  modsubi  16398  gcdmodi  16400  decexp2  16401  decsplit0b  16406  decsplit1  16408  decsplit  16409  karatsuba  16410  2exp8  16413  3exp3  16415  5prm  16432  7prm  16434  11prm  16438  prmlem2  16443  37prm  16444  43prm  16445  83prm  16446  139prm  16447  163prm  16448  317prm  16449  631prm  16450  prmo5  16452  1259lem1  16454  1259lem2  16455  1259lem3  16456  1259lem4  16457  1259lem5  16458  2503lem1  16460  2503lem2  16461  2503lem3  16462  2503prm  16463  4001lem1  16464  4001lem2  16465  4001lem3  16466  4001lem4  16467  4001prm  16468  pwsbas  16750  rcaninv  17054  subsubc  17113  xpccatid  17428  subsubm  17971  mulg2  18177  subsubg  18242  oppgmnd  18422  gsumwrev  18434  psgnunilem2  18554  sylow1lem1  18654  subgslw  18672  sylow3  18689  efginvrel2  18784  efgsfo  18796  frgpnabllem1  18924  gsumzaddlem  18972  gsummptfzsplitl  18984  gsummpt1n0  19016  dprdfid  19070  ablfac1lem  19121  pgpfac1lem3  19130  pgpfaclem1  19134  ablsimpgfindlem1  19160  mgpress  19181  srgbinomlem4  19224  opprring  19312  unitsubm  19351  subsubrg  19492  cntzsdrg  19512  subdrgint  19513  lsslss  19664  evlsval  20229  mpff  20247  coe1fzgsumdlem  20399  evl1gsumdlem  20449  xrsnsgrp  20511  gzrngunit  20541  expghm  20573  chrid  20604  zrhpsgnmhm  20658  psgndiflemA  20675  frlmip  20852  frlmphl  20855  matvsca2  20967  mattposvs  20994  m2detleiblem3  21168  m2detleiblem4  21169  cpmidpmat  21411  resstopn  21724  cnmpt1res  22214  ressuss  22801  iscusp2  22840  ucnextcn  22842  txmetcnp  23086  rerest  23341  xrtgioo  23343  xrrest  23344  cnmpopc  23461  xrhmeo  23479  clmvs2  23627  clmnegneg  23637  ncvsm1  23687  ncvspi  23689  cphassir  23748  cphipval2  23773  reust  23913  rrxprds  23921  csbren  23931  rrxdsfi  23943  minveclem2  23958  ovolunlem1a  24026  ovolicc2lem4  24050  uniioombllem5  24117  iblabs  24358  iblabsr  24359  iblmulc2  24360  itgmulc2  24363  limcres  24413  dvfval  24424  dvreslem  24436  dvres2lem  24437  dvcnp2  24446  cpnres  24463  dvcobr  24472  dveflem  24505  lhop1lem  24539  lhop2  24541  dvcnvrelem2  24544  plyun0  24716  coeeulem  24743  coeeu  24744  dvply1  24802  dvtaylp  24887  taylthlem2  24891  taylth  24892  dvradcnv  24938  pserdvlem2  24945  abelthlem8  24956  abelth  24958  sinhalfpilem  24978  cospi  24987  eulerid  24989  cos2pi  24991  ef2kpi  24993  sinhalfpip  25007  sinhalfpim  25008  coshalfpip  25009  coshalfpim  25010  sincosq3sgn  25015  sincosq4sgn  25016  tangtx  25020  sincos4thpi  25028  sincos6thpi  25030  sineq0  25038  tanregt0  25050  logm1  25099  abslogle  25128  tanarg  25129  logcnlem4  25155  advlogexp  25165  cxpsqrt  25213  dvsqrt  25250  dvcnsqrt  25252  cxpcn3  25256  root1cj  25264  cxpeq  25265  logb1  25274  2logb9irr  25300  sqrt2cxp2logb9e3  25304  ang180lem1  25314  ang180lem2  25315  ang180lem3  25316  lawcos  25321  isosctrlem1  25323  isosctrlem2  25324  quad2  25344  1cubrlem  25346  1cubr  25347  dcubic2  25349  mcubic  25352  binom4  25355  dquartlem1  25356  quart1lem  25360  quart1  25361  quartlem1  25362  asinlem  25373  asinlem2  25374  asinlem3a  25375  acosneg  25392  efiasin  25393  asinsinlem  25396  asinsin  25397  acoscos  25398  asin1  25399  acosbnd  25405  atancj  25415  efiatan  25417  atanlogaddlem  25418  efiatan2  25422  2efiatan  25423  tanatan  25424  cosatan  25426  atantan  25428  atanbndlem  25430  atans2  25436  dvatan  25440  atantayl  25442  atantayl2  25443  log2cnv  25450  log2tlbnd  25451  log2ublem2  25453  log2ublem3  25454  log2ub  25455  birthday  25460  jensenlem1  25492  amgmlem  25495  lgamgulmlem2  25535  lgamgulmlem5  25538  lgambdd  25542  ftalem2  25579  ftalem5  25582  ftalem6  25583  basellem2  25587  basellem3  25588  basellem5  25590  basellem8  25593  basellem9  25594  mule1  25653  ppi1i  25673  musum  25696  ppiublem1  25706  ppiub  25708  chtublem  25715  chtub  25716  dchrptlem1  25768  dchrptlem2  25769  bclbnd  25784  bposlem6  25793  bposlem8  25795  bposlem9  25796  lgsdir2lem1  25829  lgsdir2lem2  25830  lgsdir2lem4  25832  lgsdir2lem5  25833  lgsne0  25839  1lgs  25844  gausslemma2dlem0e  25864  gausslemma2dlem0f  25865  gausslemma2dlem3  25872  gausslemma2d  25878  lgseisenlem1  25879  lgseisenlem2  25880  lgseisenlem3  25881  lgseisenlem4  25882  lgseisen  25883  lgsquadlem1  25884  lgsquadlem2  25885  lgsquad2lem1  25888  lgsquad2lem2  25889  m1lgs  25892  2lgslem3a  25900  2lgslem3b  25901  2lgslem3c  25902  2lgslem3d  25903  2lgsoddprmlem3a  25914  2lgsoddprmlem3b  25915  2lgsoddprmlem3c  25916  2lgsoddprmlem3d  25917  addsqnreup  25947  chebbnd1lem2  25974  chebbnd1lem3  25975  rplogsumlem2  25989  dchrisum0flblem1  26012  dchrisum0re  26017  mulog2sumlem2  26039  chpdifbndlem1  26057  pntpbnd1a  26089  pntpbnd2  26091  pntibndlem2  26095  pntibndlem3  26096  pntlemg  26102  pntlemk  26110  pntlemo  26111  axsegconlem1  26631  ax5seglem7  26649  axlowdimlem3  26658  axlowdimlem16  26671  axlowdimlem17  26672  elntg2  26699  vdegp1bi  27247  vtxdginducedm1  27253  wlkp1lem1  27383  spthispth  27435  2wlkdlem1  27632  2pthd  27647  clwlkclwwlkfo  27715  3wlkdlem1  27866  3pthd  27881  eucrct2eupth  27952  numclwwlk5  28095  numclwwlk7  28098  frgrregord013  28102  ex-fl  28154  ex-mod  28156  ex-exp  28157  ex-bc  28159  ex-lcm  28165  ex-ind-dvds  28168  vc2OLD  28273  vc0  28279  vcm  28281  nvm1  28370  nvpi  28372  nvmtri  28376  nvge0  28378  ipval3  28414  ipidsq  28415  ip0i  28530  ip1ilem  28531  ip2i  28533  ipdirilem  28534  ipasslem10  28544  siilem1  28556  siii  28558  minvecolem2  28580  hvsubid  28731  hvaddsubval  28738  hvmul2negi  28753  hvadd12i  28762  hv2times  28766  hvnegdii  28767  hvaddcani  28770  hi01  28801  hisubcomi  28809  normlem0  28814  normlem1  28815  normlem3  28817  normlem9  28823  bcseqi  28825  normsqi  28837  norm-ii-i  28842  normsubi  28846  norm3difi  28852  norm3adifii  28853  normpar2i  28861  polid2i  28862  polidi  28863  chdmm2i  29183  chj12i  29227  spanunsni  29284  qlaxr5i  29340  osumcor2i  29349  spansnji  29351  pjadjii  29379  pjinormii  29381  pjsslem  29384  pjpythi  29427  mayete3i  29433  mayetes3i  29434  hoadd12i  29482  honegneg  29511  ho2times  29524  hoaddsubi  29526  hosd1i  29527  hosd2i  29528  honpncani  29532  lnopeq0lem1  29710  lnopunilem1  29715  lnophmlem2  29722  lnfn0i  29747  nmopcoadji  29806  nmopcoadj2i  29807  opsqrlem1  29845  opsqrlem5  29849  opsqrlem6  29850  pjclem3  29902  stadd3i  29953  mddmd2  30014  mdexchi  30040  cvexchlem  30073  atomli  30087  atordi  30089  atabs2i  30107  mdsymlem1  30108  iuninc  30241  suppss2f  30313  suppss3  30387  dfdec100  30474  dpfrac1  30496  decdiv10  30500  dpmul100  30501  dp3mul10  30502  dpmul1000  30503  dpexpp1  30512  dpadd2  30514  dpadd  30515  dpmul  30517  dpmul4  30518  threehalves  30519  1mhdrd  30520  pfxlsw2ccat  30554  cyc2fv1  30691  cyc2fv2  30692  cycpmco2lem4  30699  cycpmco2lem5  30700  cyc3fv1  30707  cyc3fv2  30708  cyc3fv3  30709  archirngz  30746  gsumvsca2  30783  nn0omnd  30842  nn0archi  30844  xrge0slmod  30845  fedgmullem1  30925  fedgmullem2  30926  fedgmul  30927  lmatfvlem  30980  sqsscirc1  31051  cnvordtrestixx  31056  raddcn  31072  xrge0iifhom  31080  xrge0mulc1cn  31084  xrge0tmd  31088  lmlimxrge0  31091  qqhucn  31133  rrhcn  31138  qqtopn  31152  rrhqima  31155  brfae  31407  inelcarsg  31469  cndprobnul  31595  isrrvv  31601  ballotlem1  31644  ballotlem2  31646  ballotlemi1  31660  ballotlemii  31661  ballotlemic  31664  ballotlem1c  31665  ballotlemfrceq  31686  ballotth  31695  ofcs2  31715  signsvtn0  31740  signstfveq0  31747  signsvtp  31753  signsvtn  31754  signsvfpn  31755  signsvfnn  31756  signshf  31758  hashreprin  31791  reprfz1  31795  chtvalz  31800  breprexp  31804  breprexpnat  31805  hgt750lemd  31819  hgt750lem  31822  hgt750lem2  31823  subfacp1lem1  32324  subfacp1lem5  32329  subfacp1lem6  32330  subfaclim  32333  cvmliftlem5  32434  cvmliftlem8  32437  cvmliftlem10  32439  cvmliftlem13  32441  cvmlift2lem6  32453  cvmlift2lem12  32459  problem1  32806  problem2  32807  problem4  32809  quad3  32811  iexpire  32865  sin2h  34764  poimirlem16  34790  poimirlem17  34791  poimirlem18  34792  poimirlem19  34793  poimirlem20  34794  poimirlem21  34795  poimirlem22  34796  poimirlem26  34800  mblfinlem3  34813  ismblfin  34815  itg2addnclem3  34827  iblabsnc  34838  iblmulc2nc  34839  itgmulc2nc  34842  ftc1cnnc  34848  ftc1anclem6  34854  ftc1anclem7  34855  ftc1anclem8  34856  dvasin  34860  fdc  34903  heiborlem4  34975  heiborlem6  34977  dalem24  36715  pmod2iN  36867  cdleme9  37271  cdleme20aN  37327  cdleme22e  37362  cdleme22eALTN  37363  cdleme25cv  37376  cdleme29b  37393  cdlemh1  37833  cdlemh2  37834  cdlemk35  37930  cdlemkid1  37940  sqmid3api  39049  sqn5i  39051  sqdeccom12  39055  235t711  39057  nn0expgcd  39064  re1m1e0m0  39107  readdid2  39113  remul02  39115  pellexlem5  39310  reglog1  39373  jm2.23  39473  jm2.27c  39484  lnmlsslnm  39561  lmhmlnmsplit  39567  areaquad  39703  cotrclrcl  39967  inductionexd  40385  hashnzfz2  40533  lhe4.4ex1a  40541  binomcxplemdvsum  40567  binomcxplemnotnn0  40568  binomcxp  40569  sineq0ALT  41151  unirnmapsn  41357  fzisoeu  41447  fsummulc1f  41731  fprodexp  41755  constlimc  41785  sumnnodd  41791  limcresiooub  41803  limcresioolb  41804  cncfshiftioo  42055  fperdvper  42083  dvnmul  42108  dvmptfprod  42110  itgsinexplem1  42119  stoweidlem11  42177  stoweidlem13  42179  stoweidlem26  42192  stoweidlem34  42200  wallispilem4  42234  wallispi2lem1  42237  wallispi2lem2  42238  stirlinglem11  42250  dirkerper  42262  dirkertrigeqlem1  42264  dirkertrigeqlem3  42266  dirkercncflem1  42269  dirkercncflem4  42272  fourierdlem30  42303  fourierdlem32  42305  fourierdlem33  42306  fourierdlem42  42315  fourierdlem46  42318  fourierdlem47  42319  fourierdlem57  42329  fourierdlem60  42332  fourierdlem61  42333  fourierdlem62  42334  fourierdlem68  42340  fourierdlem73  42345  fourierdlem79  42351  fourierdlem89  42361  fourierdlem90  42362  fourierdlem91  42363  fourierdlem96  42368  fourierdlem97  42369  fourierdlem98  42370  fourierdlem99  42371  fourierdlem100  42372  fourierdlem103  42375  fourierdlem104  42376  fourierdlem108  42380  fourierdlem110  42382  fourierdlem113  42385  sqwvfoura  42394  sqwvfourb  42395  fourierswlem  42396  fouriersw  42397  fouriercn  42398  etransclem4  42404  etransclem7  42407  etransclem23  42423  etransclem24  42424  etransclem25  42425  etransclem26  42426  etransclem31  42431  etransclem32  42432  etransclem35  42435  etransclem37  42437  etransclem46  42446  rrndistlt  42456  sge0tsms  42543  sge0xaddlem2  42597  vonioolem2  42844  1t10e1p1e11  43391  deccarry  43392  1fzopredsuc  43405  m1mod0mod1  43410  iccpartgt  43434  fmtno0  43549  fmtno1  43550  fmtnorec2  43552  fmtno2  43559  fmtno3  43560  fmtno4  43561  fmtno5  43566  257prm  43570  fmtnofac1  43579  fmtno4prmfac  43581  fmtno4prmfac193  43582  fmtno4nprmfac193  43583  m2prm  43600  m3prm  43601  flsqrt5  43604  3ndvds4  43605  139prmALT  43606  31prm  43607  2exp7  43609  127prm  43610  m11nprm  43613  lighneallem2  43618  lighneallem3  43619  3exp4mod41  43628  41prothprmlem1  43629  41prothprmlem2  43630  41prothprm  43631  m1expevenALTV  43659  1oddALTV  43702  6even  43723  8even  43725  2exp340mod341  43745  341fppr2  43746  4fppr1  43747  8exp8mod9  43748  9fppr8  43749  nfermltl8rev  43754  gbpart7  43779  gbpart9  43781  gbpart11  43782  sbgoldbo  43799  bgoldbtbndlem1  43817  tgoldbachlt  43828  subsubmgm  43911  smndex2dnrinv  43985  altgsumbcALT  44299  lincfsuppcl  44366  linccl  44367  lincvalsn  44370  lincdifsn  44377  lincsum  44382  lincscm  44383  lindslinindimp2lem4  44414  lindslinindsimp2lem5  44415  snlindsntor  44424  lincresunit3lem2  44433  zlmodzxzldeplem3  44455  ldepsnlinc  44461  nn0sumshdiglemA  44577  nn0sumshdiglemB  44578  affinecomb1  44587  rrx2linest  44627  itschlc0yqe  44645  itsclc0yqsollem1  44647  itscnhlc0xyqsol  44650  itschlc0xyqsol1  44651  itsclquadb  44661  2itscplem2  44664  itscnhlinecirc02plem2  44668  sinh-conventional  44736  onetansqsecsq  44758  cotsqcscsq  44759  mvlraddi  44769  mvrladdi  44770  mvlrmuli  44776  amgmwlem  44801  amgmlemALT  44802
  Copyright terms: Public domain W3C validator