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

Theorem oveq1i 7158
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 7155 . 2 (𝐴 = 𝐵 → (𝐴𝐹𝐶) = (𝐵𝐹𝐶))
31, 2ax-mp 5 1 (𝐴𝐹𝐶) = (𝐵𝐹𝐶)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1530  (class class class)co 7148
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2798
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2805  df-cleq 2819  df-clel 2898  df-nfc 2968  df-rex 3149  df-rab 3152  df-v 3502  df-dif 3943  df-un 3945  df-in 3947  df-ss 3956  df-nul 4296  df-if 4471  df-sn 4565  df-pr 4567  df-op 4571  df-uni 4838  df-br 5064  df-iota 6312  df-fv 6360  df-ov 7151
This theorem is referenced by:  caov12  7366  caov411  7370  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  17966  mulg2  18167  subsubg  18232  oppgmnd  18412  gsumwrev  18424  psgnunilem2  18543  sylow1lem1  18643  subgslw  18661  sylow3  18678  efginvrel2  18773  efgsfo  18785  frgpnabllem1  18913  gsumzaddlem  18961  gsummptfzsplitl  18973  gsummpt1n0  19005  dprdfid  19059  ablfac1lem  19110  pgpfac1lem3  19119  pgpfaclem1  19123  ablsimpgfindlem1  19149  mgpress  19170  srgbinomlem4  19213  opprring  19301  unitsubm  19340  subsubrg  19481  cntzsdrg  19501  subdrgint  19502  lsslss  19653  evlsval  20217  mpff  20234  coe1fzgsumdlem  20386  evl1gsumdlem  20435  xrsnsgrp  20497  gzrngunit  20527  expghm  20559  chrid  20590  zrhpsgnmhm  20644  psgndiflemA  20661  frlmip  20838  frlmphl  20841  matvsca2  20953  mattposvs  20980  m2detleiblem3  21154  m2detleiblem4  21155  cpmidpmat  21397  resstopn  21710  cnmpt1res  22200  ressuss  22787  iscusp2  22826  ucnextcn  22828  txmetcnp  23072  rerest  23327  xrtgioo  23329  xrrest  23330  cnmpopc  23447  xrhmeo  23465  clmvs2  23613  clmnegneg  23623  ncvsm1  23673  ncvspi  23675  cphassir  23734  cphipval2  23759  reust  23899  rrxprds  23907  csbren  23917  rrxdsfi  23929  minveclem2  23944  ovolunlem1a  24012  ovolicc2lem4  24036  uniioombllem5  24103  iblabs  24344  iblabsr  24345  iblmulc2  24346  itgmulc2  24349  limcres  24399  dvfval  24410  dvreslem  24422  dvres2lem  24423  dvcnp2  24432  cpnres  24449  dvcobr  24458  dveflem  24491  lhop1lem  24525  lhop2  24527  dvcnvrelem2  24530  plyun0  24702  coeeulem  24729  coeeu  24730  dvply1  24788  dvtaylp  24873  taylthlem2  24877  taylth  24878  dvradcnv  24924  pserdvlem2  24931  abelthlem8  24942  abelth  24944  sinhalfpilem  24964  cospi  24973  eulerid  24975  cos2pi  24977  ef2kpi  24979  sinhalfpip  24993  sinhalfpim  24994  coshalfpip  24995  coshalfpim  24996  sincosq3sgn  25001  sincosq4sgn  25002  tangtx  25006  sincos4thpi  25014  sincos6thpi  25016  sineq0  25024  tanregt0  25036  logm1  25085  abslogle  25114  tanarg  25115  logcnlem4  25141  advlogexp  25151  cxpsqrt  25199  dvsqrt  25236  dvcnsqrt  25238  cxpcn3  25242  root1cj  25250  cxpeq  25251  logb1  25260  2logb9irr  25286  sqrt2cxp2logb9e3  25290  ang180lem1  25300  ang180lem2  25301  ang180lem3  25302  lawcos  25307  isosctrlem1  25309  isosctrlem2  25310  quad2  25330  1cubrlem  25332  1cubr  25333  dcubic2  25335  mcubic  25338  binom4  25341  dquartlem1  25342  quart1lem  25346  quart1  25347  quartlem1  25348  asinlem  25359  asinlem2  25360  asinlem3a  25361  acosneg  25378  efiasin  25379  asinsinlem  25382  asinsin  25383  acoscos  25384  asin1  25385  acosbnd  25391  atancj  25401  efiatan  25403  atanlogaddlem  25404  efiatan2  25408  2efiatan  25409  tanatan  25410  cosatan  25412  atantan  25414  atanbndlem  25416  atans2  25422  dvatan  25426  atantayl  25428  atantayl2  25429  log2cnv  25436  log2tlbnd  25437  log2ublem2  25439  log2ublem3  25440  log2ub  25441  birthday  25446  jensenlem1  25478  amgmlem  25481  lgamgulmlem2  25521  lgamgulmlem5  25524  lgambdd  25528  ftalem2  25565  ftalem5  25568  ftalem6  25569  basellem2  25573  basellem3  25574  basellem5  25576  basellem8  25579  basellem9  25580  mule1  25639  ppi1i  25659  musum  25682  ppiublem1  25692  ppiub  25694  chtublem  25701  chtub  25702  dchrptlem1  25754  dchrptlem2  25755  bclbnd  25770  bposlem6  25779  bposlem8  25781  bposlem9  25782  lgsdir2lem1  25815  lgsdir2lem2  25816  lgsdir2lem4  25818  lgsdir2lem5  25819  lgsne0  25825  1lgs  25830  gausslemma2dlem0e  25850  gausslemma2dlem0f  25851  gausslemma2dlem3  25858  gausslemma2d  25864  lgseisenlem1  25865  lgseisenlem2  25866  lgseisenlem3  25867  lgseisenlem4  25868  lgseisen  25869  lgsquadlem1  25870  lgsquadlem2  25871  lgsquad2lem1  25874  lgsquad2lem2  25875  m1lgs  25878  2lgslem3a  25886  2lgslem3b  25887  2lgslem3c  25888  2lgslem3d  25889  2lgsoddprmlem3a  25900  2lgsoddprmlem3b  25901  2lgsoddprmlem3c  25902  2lgsoddprmlem3d  25903  addsqnreup  25933  chebbnd1lem2  25960  chebbnd1lem3  25961  rplogsumlem2  25975  dchrisum0flblem1  25998  dchrisum0re  26003  mulog2sumlem2  26025  chpdifbndlem1  26043  pntpbnd1a  26075  pntpbnd2  26077  pntibndlem2  26081  pntibndlem3  26082  pntlemg  26088  pntlemk  26096  pntlemo  26097  axsegconlem1  26617  ax5seglem7  26635  axlowdimlem3  26644  axlowdimlem16  26657  axlowdimlem17  26658  elntg2  26685  vdegp1bi  27233  vtxdginducedm1  27239  wlkp1lem1  27369  spthispth  27421  2wlkdlem1  27618  2pthd  27633  clwlkclwwlkfo  27701  3wlkdlem1  27852  3pthd  27867  eucrct2eupth  27938  numclwwlk5  28081  numclwwlk7  28084  frgrregord013  28088  ex-fl  28140  ex-mod  28142  ex-exp  28143  ex-bc  28145  ex-lcm  28151  ex-ind-dvds  28154  vc2OLD  28259  vc0  28265  vcm  28267  nvm1  28356  nvpi  28358  nvmtri  28362  nvge0  28364  ipval3  28400  ipidsq  28401  ip0i  28516  ip1ilem  28517  ip2i  28519  ipdirilem  28520  ipasslem10  28530  siilem1  28542  siii  28544  minvecolem2  28566  hvsubid  28717  hvaddsubval  28724  hvmul2negi  28739  hvadd12i  28748  hv2times  28752  hvnegdii  28753  hvaddcani  28756  hi01  28787  hisubcomi  28795  normlem0  28800  normlem1  28801  normlem3  28803  normlem9  28809  bcseqi  28811  normsqi  28823  norm-ii-i  28828  normsubi  28832  norm3difi  28838  norm3adifii  28839  normpar2i  28847  polid2i  28848  polidi  28849  chdmm2i  29169  chj12i  29213  spanunsni  29270  qlaxr5i  29326  osumcor2i  29335  spansnji  29337  pjadjii  29365  pjinormii  29367  pjsslem  29370  pjpythi  29413  mayete3i  29419  mayetes3i  29420  hoadd12i  29468  honegneg  29497  ho2times  29510  hoaddsubi  29512  hosd1i  29513  hosd2i  29514  honpncani  29518  lnopeq0lem1  29696  lnopunilem1  29701  lnophmlem2  29708  lnfn0i  29733  nmopcoadji  29792  nmopcoadj2i  29793  opsqrlem1  29831  opsqrlem5  29835  opsqrlem6  29836  pjclem3  29888  stadd3i  29939  mddmd2  30000  mdexchi  30026  cvexchlem  30059  atomli  30073  atordi  30075  atabs2i  30093  mdsymlem1  30094  iuninc  30227  suppss2f  30299  suppss3  30373  dfdec100  30460  dpfrac1  30482  decdiv10  30486  dpmul100  30487  dp3mul10  30488  dpmul1000  30489  dpexpp1  30498  dpadd2  30500  dpadd  30501  dpmul  30503  dpmul4  30504  threehalves  30505  1mhdrd  30506  pfxlsw2ccat  30540  cyc2fv1  30677  cyc2fv2  30678  cycpmco2lem4  30685  cycpmco2lem5  30686  cyc3fv1  30693  cyc3fv2  30694  cyc3fv3  30695  archirngz  30732  gsumvsca2  30769  nn0omnd  30828  nn0archi  30830  xrge0slmod  30831  fedgmullem1  30911  fedgmullem2  30912  fedgmul  30913  lmatfvlem  30966  sqsscirc1  31037  cnvordtrestixx  31042  raddcn  31058  xrge0iifhom  31066  xrge0mulc1cn  31070  xrge0tmd  31074  lmlimxrge0  31077  qqhucn  31119  rrhcn  31124  qqtopn  31138  rrhqima  31141  brfae  31393  inelcarsg  31455  cndprobnul  31581  isrrvv  31587  ballotlem1  31630  ballotlem2  31632  ballotlemi1  31646  ballotlemii  31647  ballotlemic  31650  ballotlem1c  31651  ballotlemfrceq  31672  ballotth  31681  ofcs2  31701  signsvtn0  31726  signstfveq0  31733  signsvtp  31739  signsvtn  31740  signsvfpn  31741  signsvfnn  31742  signshf  31744  hashreprin  31777  reprfz1  31781  chtvalz  31786  breprexp  31790  breprexpnat  31791  hgt750lemd  31805  hgt750lem  31808  hgt750lem2  31809  subfacp1lem1  32310  subfacp1lem5  32315  subfacp1lem6  32316  subfaclim  32319  cvmliftlem5  32420  cvmliftlem8  32423  cvmliftlem10  32425  cvmliftlem13  32427  cvmlift2lem6  32439  cvmlift2lem12  32445  problem1  32792  problem2  32793  problem4  32795  quad3  32797  iexpire  32851  sin2h  34749  poimirlem16  34775  poimirlem17  34776  poimirlem18  34777  poimirlem19  34778  poimirlem20  34779  poimirlem21  34780  poimirlem22  34781  poimirlem26  34785  mblfinlem3  34798  ismblfin  34800  itg2addnclem3  34812  iblabsnc  34823  iblmulc2nc  34824  itgmulc2nc  34827  ftc1cnnc  34833  ftc1anclem6  34839  ftc1anclem7  34840  ftc1anclem8  34841  dvasin  34845  fdc  34888  heiborlem4  34960  heiborlem6  34962  dalem24  36700  pmod2iN  36852  cdleme9  37256  cdleme20aN  37312  cdleme22e  37347  cdleme22eALTN  37348  cdleme25cv  37361  cdleme29b  37378  cdlemh1  37818  cdlemh2  37819  cdlemk35  37915  cdlemkid1  37925  sqmid3api  39034  sqn5i  39036  sqdeccom12  39040  235t711  39042  nn0expgcd  39049  re1m1e0m0  39092  readdid2  39098  remul02  39100  pellexlem5  39295  reglog1  39358  jm2.23  39458  jm2.27c  39469  lnmlsslnm  39546  lmhmlnmsplit  39552  areaquad  39688  cotrclrcl  39952  inductionexd  40370  hashnzfz2  40518  lhe4.4ex1a  40526  binomcxplemdvsum  40552  binomcxplemnotnn0  40553  binomcxp  40554  sineq0ALT  41136  unirnmapsn  41342  fzisoeu  41432  fsummulc1f  41716  fprodexp  41740  constlimc  41770  sumnnodd  41776  limcresiooub  41788  limcresioolb  41789  cncfshiftioo  42040  fperdvper  42068  dvnmul  42093  dvmptfprod  42095  itgsinexplem1  42104  stoweidlem11  42162  stoweidlem13  42164  stoweidlem26  42177  stoweidlem34  42185  wallispilem4  42219  wallispi2lem1  42222  wallispi2lem2  42223  stirlinglem11  42235  dirkerper  42247  dirkertrigeqlem1  42249  dirkertrigeqlem3  42251  dirkercncflem1  42254  dirkercncflem4  42257  fourierdlem30  42288  fourierdlem32  42290  fourierdlem33  42291  fourierdlem42  42300  fourierdlem46  42303  fourierdlem47  42304  fourierdlem57  42314  fourierdlem60  42317  fourierdlem61  42318  fourierdlem62  42319  fourierdlem68  42325  fourierdlem73  42330  fourierdlem79  42336  fourierdlem89  42346  fourierdlem90  42347  fourierdlem91  42348  fourierdlem96  42353  fourierdlem97  42354  fourierdlem98  42355  fourierdlem99  42356  fourierdlem100  42357  fourierdlem103  42360  fourierdlem104  42361  fourierdlem108  42365  fourierdlem110  42367  fourierdlem113  42370  sqwvfoura  42379  sqwvfourb  42380  fourierswlem  42381  fouriersw  42382  fouriercn  42383  etransclem4  42389  etransclem7  42392  etransclem23  42408  etransclem24  42409  etransclem25  42410  etransclem26  42411  etransclem31  42416  etransclem32  42417  etransclem35  42420  etransclem37  42422  etransclem46  42431  rrndistlt  42441  sge0tsms  42528  sge0xaddlem2  42582  vonioolem2  42829  1t10e1p1e11  43376  deccarry  43377  1fzopredsuc  43390  m1mod0mod1  43395  iccpartgt  43419  fmtno0  43534  fmtno1  43535  fmtnorec2  43537  fmtno2  43544  fmtno3  43545  fmtno4  43546  fmtno5  43551  257prm  43555  fmtnofac1  43564  fmtno4prmfac  43566  fmtno4prmfac193  43567  fmtno4nprmfac193  43568  m2prm  43585  m3prm  43586  flsqrt5  43589  3ndvds4  43590  139prmALT  43591  31prm  43592  2exp7  43594  127prm  43595  m11nprm  43598  lighneallem2  43603  lighneallem3  43604  3exp4mod41  43613  41prothprmlem1  43614  41prothprmlem2  43615  41prothprm  43616  m1expevenALTV  43644  1oddALTV  43687  6even  43708  8even  43710  2exp340mod341  43730  341fppr2  43731  4fppr1  43732  8exp8mod9  43733  9fppr8  43734  nfermltl8rev  43739  gbpart7  43764  gbpart9  43766  gbpart11  43767  sbgoldbo  43784  bgoldbtbndlem1  43802  tgoldbachlt  43813  subsubmgm  43896  altgsumbcALT  44233  lincfsuppcl  44300  linccl  44301  lincvalsn  44304  lincdifsn  44311  lincsum  44316  lincscm  44317  lindslinindimp2lem4  44348  lindslinindsimp2lem5  44349  snlindsntor  44358  lincresunit3lem2  44367  zlmodzxzldeplem3  44389  ldepsnlinc  44395  nn0sumshdiglemA  44511  nn0sumshdiglemB  44512  affinecomb1  44521  rrx2linest  44561  itschlc0yqe  44579  itsclc0yqsollem1  44581  itscnhlc0xyqsol  44584  itschlc0xyqsol1  44585  itsclquadb  44595  2itscplem2  44598  itscnhlinecirc02plem2  44602  sinh-conventional  44670  onetansqsecsq  44692  cotsqcscsq  44693  mvlraddi  44703  mvrladdi  44704  mvlrmuli  44710  amgmwlem  44735  amgmlemALT  44736
  Copyright terms: Public domain W3C validator