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

Theorem oveq2i 6626
Description: Equality inference for operation value. (Contributed by NM, 28-Feb-1995.)
Hypothesis
Ref Expression
oveq1i.1 𝐴 = 𝐵
Assertion
Ref Expression
oveq2i (𝐶𝐹𝐴) = (𝐶𝐹𝐵)

Proof of Theorem oveq2i
StepHypRef Expression
1 oveq1i.1 . 2 𝐴 = 𝐵
2 oveq2 6623 . 2 (𝐴 = 𝐵 → (𝐶𝐹𝐴) = (𝐶𝐹𝐵))
31, 2ax-mp 5 1 (𝐶𝐹𝐴) = (𝐶𝐹𝐵)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1480  (class class class)co 6615
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-rex 2914  df-rab 2917  df-v 3192  df-dif 3563  df-un 3565  df-in 3567  df-ss 3574  df-nul 3898  df-if 4065  df-sn 4156  df-pr 4158  df-op 4162  df-uni 4410  df-br 4624  df-iota 5820  df-fv 5865  df-ov 6618
This theorem is referenced by:  caov32  6826  caov4  6830  caov42  6832  seqomsuc  7512  oa1suc  7571  o2p2e4  7581  om1  7582  oe1  7584  oawordeulem  7594  oeoalem  7636  nnm1  7688  nnm2  7689  nneob  7692  omopthlem1  7695  mapsnconst  7863  mapsncnv  7864  map2xp  8090  cantnflt  8529  cnfcom2  8559  infxpenc  8801  infxpenc2  8805  ackbij1lem5  9006  alephom  9367  pwxpndom2  9447  adderpqlem  9736  addassnq  9740  mulcanenq  9742  distrnq  9743  ltanq  9753  ltexnq  9757  halfnq  9758  ltrnq  9761  archnq  9762  addclprlem2  9799  prlem934  9815  prlem936  9829  addcmpblnr  9850  mulcmpblnrlem  9851  ltsrpr  9858  m1p1sr  9873  m1m1sr  9874  0idsr  9878  1idsr  9879  00sr  9880  pn0sr  9882  recexsrlem  9884  mulgt0sr  9886  sqgt0sr  9887  mulresr  9920  axmulcom  9936  axmulass  9938  axdistr  9939  axi2m1  9940  ax1rid  9942  axcnre  9945  mul02lem1  10172  addid1  10176  negid  10288  negsub  10289  subneg  10290  negsubdii  10326  muleqadd  10631  crne0  10973  2p2e4  11104  3p2e5  11120  3p3e6  11121  4p2e6  11122  4p3e7  11123  4p4e8  11124  5p2e7  11125  5p3e8  11126  5p4e9  11127  5p5e10OLD  11128  6p2e8  11129  6p3e9  11130  6p4e10OLD  11131  7p2e9  11132  7p3e10OLD  11133  8p2e10OLD  11134  3t3e9  11140  8th4div3  11212  halfpm6th  11213  addltmul  11228  div4p1lem1div2  11247  nn0n0n1ge2  11318  nneo  11421  zeo  11423  numsuc  11471  numltc  11488  numsucc  11509  numma  11517  nummul1c  11522  decrmac  11537  decsubi  11543  decsubiOLD  11544  decmul1  11545  decmul10add  11553  decmul10addOLD  11554  6p5lem  11555  5p5e10  11556  6p4e10  11558  7p3e10  11563  8p2e10  11570  4t3lem  11591  9t11e99  11631  9t11e99OLD  11632  decbin2  11643  xmulmnf1  12065  fztp  12355  fzprval  12359  fztpval  12360  fzshftral  12385  fz0tp  12397  fz0to3un2pr  12398  fzo01  12507  fzo12sn  12508  fzo13pr  12509  fzo0to2pr  12510  fzo0to3tp  12511  fzo0to42pr  12512  fzo1to4tp  12513  quoremz  12610  quoremnn0ALT  12612  intfrac2  12613  intfracq  12614  sqval  12878  sqrecii  12902  sq4e2t8  12918  cu2  12919  i3  12922  i4  12923  binom2i  12930  binom3  12941  crreczi  12945  3dec  13006  sq10OLD  13007  3decOLD  13009  nn0opthlem1  13011  facp1  13021  faclbnd  13033  faclbnd2  13034  faclbnd4lem1  13036  faclbnd4lem4  13039  bcn1  13056  bcn2  13062  4bc3eq4  13071  4bc2eq6  13072  hashgadd  13122  hashxplem  13176  hashmap  13178  hashfun  13180  hashbclem  13190  fz1isolem  13199  ccatlid  13324  ccatrid  13325  ccats1val2  13358  ccat2s1p2  13360  wrdeqs1cat  13428  swrdccatin12lem3  13443  swrdccat3a  13447  cats1fvn  13556  cats1cat  13559  cats2cat  13560  s3fn  13608  swrds2  13635  reim0  13808  cji  13849  sqrtm1  13966  absi  13976  rddif  14030  iseraltlem2  14363  iseralt  14365  fsump1i  14447  fsummulc2  14463  incexclem  14512  incexc  14513  arisum2  14537  geoihalfsum  14558  mertenslem1  14560  mertens  14562  risefall0lem  14701  risefac1  14708  fallfac1  14709  fallfacfwd  14711  bpoly0  14725  bpoly1  14726  bpolydiflem  14729  bpoly2  14732  bpoly3  14733  bpoly4  14734  fsumcube  14735  ef0lem  14753  ege2le3  14764  eft0val  14786  ef4p  14787  efgt1p2  14788  efgt1p  14789  tanval2  14807  efival  14826  ef01bndlem  14858  sin01bnd  14859  cos01bnd  14860  cos1bnd  14861  cos2bnd  14862  rpnnen2lem11  14897  sqr2irrlem  14921  3dvdsdec  14997  3dvdsdecOLD  14998  3dvds2dec  14999  3dvds2decOLD  15000  odd2np1lem  15007  odd2np1  15008  oddp1even  15011  opoe  15030  divalglem5  15063  divalglem6  15064  bits0  15093  0bits  15104  gcdaddmlem  15188  6gcd4e2  15198  lcmneg  15259  3lcm2e6woprm  15271  6lcm4e12  15272  3prm  15349  3lcm2e6  15383  phiprm  15425  eulerthlem2  15430  prmdiv  15433  pythagtriplem12  15474  pythagtriplem14  15476  pcmpt  15539  pcfac  15546  prmpwdvds  15551  pockthi  15554  prmreclem2  15564  prmreclem6  15568  4sqlem5  15589  4sqlem13  15604  modxai  15715  mod2xnegi  15718  gcdi  15720  decexp2  15722  numexpp1  15725  numexp2x  15726  decsplit0b  15727  decsplit1  15729  decsplit  15730  decsplit0bOLD  15731  decsplit1OLD  15733  decsplitOLD  15734  2exp16  15740  prmlem0  15755  139prm  15774  163prm  15775  317prm  15776  631prm  15777  1259lem4  15784  1259lem5  15785  1259prm  15786  2503lem1  15787  2503lem2  15788  2503lem3  15789  2503prm  15790  4001lem1  15791  4001lem4  15794  ressinbas  15876  rcaninv  16394  rescfth  16537  xpccatid  16768  oduval  17070  oppgmnd  17724  psgnunilem2  17855  psgnunilem4  17857  psgnpmtr  17870  psgn0fv0  17871  psgnsn  17880  psgnprfval1  17882  lsmmod2  18029  efgi0  18073  efgi1  18074  efginvrel2  18080  efgsval2  18086  efgsp1  18090  efgredleme  18096  efgredlemc  18098  efgcpbllemb  18108  frgpnabllem1  18216  lt6abl  18236  gsumconstf  18275  gsum2dlem2  18310  pwsgsum  18318  fsfnn0gsumfsffz  18319  dprd0  18370  dprdf1  18372  dprd2da  18381  ablfac1lem  18407  pgpfac1lem3  18416  pgpfaclem1  18420  srgbinomlem4  18483  opprring  18571  mulgass3  18577  evlsval  19459  mpff  19473  ply1assa  19509  gsumply1subr  19544  ply1coe  19606  coe1fzgsumdlem  19611  coe1fzgsumd  19612  gsumply1eq  19615  evl1gsumdlem  19660  evl1gsumd  19661  xrsnsgrp  19722  znbas  19832  znzrh2  19834  dsmmval2  20020  frlmip  20057  matgsum  20183  madetsumid  20207  mdetrsca  20349  mdetrsca2  20350  mdettpos  20357  m2detleiblem2  20374  madugsum  20389  madurid  20390  cpmat  20454  pmatcollpwfi  20527  pmatcollpw3fi1lem1  20531  pm2mpval  20540  mp2pm2mplem5  20555  chpmat1dlem  20580  chpmat1d  20581  chpidmat  20592  cpmidpmat  20618  cpmadugsumfi  20622  chcoeffeqlem  20630  cayleyhamilton0  20634  cayleyhamiltonALT  20636  cayleyhamilton1  20637  restin  20910  imacmp  21140  conncompconn  21175  uptx  21368  cnpflf2  21744  tmdgsum2  21840  tsmsres  21887  tsmsf1o  21888  tsmsmhm  21889  prdsxmet  22114  resspwsds  22117  prdsxmslem2  22274  tngngpim  22403  metdcn2  22582  metdcn  22583  metdscn2  22600  iimulcn  22677  icchmeo  22680  xrhmeo  22685  cnrehmeo  22692  cnheiborlem  22693  evth  22698  evth2  22699  lebnumlem2  22701  reparphti  22737  pcoass  22764  pi1xfrcnv  22797  ipcau2  22973  minveclem4  23143  pjthlem1  23148  ovolunlem1a  23204  unmbl  23245  uniioombl  23297  iblitg  23475  dfitg  23476  itg0  23486  iblcnlem1  23494  itgcnlem  23496  itgabs  23541  limcdif  23580  limccnp  23595  limccnp2  23596  dvexp  23656  dvmptid  23660  dvmptc  23661  dvmptfsum  23676  dveflem  23680  dvsincos  23682  mvth  23693  dvlipcn  23695  dvivthlem1  23709  dvfsumle  23722  dvfsumlem2  23728  itgsubst  23750  tdeglem4  23758  tdeglem2  23759  plypf1  23906  plymullem1  23908  coesub  23951  dgrmulc  23965  fta1lem  24000  vieta1lem1  24003  vieta1lem2  24004  aalioulem4  24028  aaliou3lem3  24037  abelthlem2  24124  abelthlem8  24131  abelthlem9  24132  sinhalfpilem  24153  efhalfpi  24161  cospi  24162  efipi  24163  sin2pi  24165  cos2pi  24166  ef2pi  24167  sin2pim  24175  cos2pim  24176  sinmpi  24177  cosmpi  24178  sinppi  24179  cosppi  24180  sincosq4sgn  24191  tangtx  24195  sincos4thpi  24203  sincos6thpi  24205  sincos3rdpi  24206  pige3  24207  abssinper  24208  efif1olem4  24229  efifo  24231  eff1o  24233  circgrp  24236  circsubm  24237  logneg  24272  logimul  24298  logneg2  24299  dvrelog  24317  logcnlem4  24325  dvlog  24331  dvlog2  24333  logtayl  24340  1cxp  24352  ecxp  24353  cxpsqrt  24383  dvsqrt  24417  dvcnsqrt  24419  root1eq1  24430  cxpeq  24432  elogb  24442  ang180lem1  24473  ang180lem2  24474  heron  24499  1cubrlem  24502  1cubr  24503  dcubic2  24505  mcubic  24508  cubic2  24509  binom4  24511  dquartlem1  24512  dquartlem2  24513  dquart  24514  quart1lem  24516  quart1  24517  quartlem1  24518  asinsin  24553  asin1  24555  acos1  24556  atanlogsublem  24576  atanlogsub  24577  efiatan2  24578  2efiatan  24579  tanatan  24580  atanbnd  24587  atan1  24589  dvatan  24596  atantayl2  24599  leibpilem2  24602  leibpi  24603  log2cnv  24605  log2tlbnd  24606  log2ublem1  24607  log2ublem2  24608  log2ublem3  24609  log2ub  24610  birthday  24615  amgmlem  24650  emcllem5  24660  lgamgulmlem2  24690  lgamgulmlem5  24693  lgam1  24724  wilthlem2  24729  ftalem6  24738  basellem2  24742  basellem3  24743  basellem5  24745  basellem8  24748  cht1  24825  chp1  24827  1sgmprm  24858  ppiublem2  24862  ppiub  24863  chtublem  24870  chtub  24871  logfacbnd3  24882  bcp1ctr  24938  bclbnd  24939  bposlem1  24943  bposlem4  24946  bposlem6  24948  bposlem8  24950  bposlem9  24951  lgslem1  24956  lgsdir2lem1  24984  lgsdir2lem2  24985  lgsdir2lem3  24986  lgsdir2lem5  24988  lgs1  25000  gausslemma2dlem1a  25024  gausslemma2dlem3  25027  gausslemma2dlem4  25028  gausslemma2d  25033  lgseisenlem1  25034  lgseisenlem3  25036  lgsquadlem1  25039  lgsquadlem2  25040  lgsquad2lem2  25044  m1lgs  25047  2lgslem1a2  25049  2sqlem8  25085  2sqblem  25090  logdivsum  25156  mulog2sumlem2  25158  log2sumbnd  25167  selberglem1  25168  selberglem2  25169  pntrmax  25187  pntibndlem2  25214  pntibndlem3  25215  pntlemg  25221  pntlemr  25225  pntlemo  25230  ostth2lem3  25258  ostth2lem4  25259  istrkg3ld  25294  trgcgrg  25344  tgcgr4  25360  colperpexlem1  25556  ax5seglem7  25749  axlowdimlem4  25759  axlowdimlem16  25771  setsiedg  25862  vdegp1ci  26354  wlkp1lem6  26478  wlkp1lem8  26480  wlkp1  26481  uhgrwkspthlem2  26553  pthdlem1  26565  pthdlem2  26567  pthd  26568  crctcshwlkn0lem4  26608  crctcshwlkn0lem5  26609  crctcshwlkn0lem6  26610  crctcshlem4  26615  crctcshwlkn0  26616  2wlkdlem2  26725  2wlkdlem4  26727  2pthdlem1  26729  clwlkclwwlk2  26805  wwlksext2clwwlk  26824  0ewlk  26875  1ewlk  26876  0wlk  26877  1pthdlem1  26895  1pthdlem2  26896  1wlkdlem1  26897  1wlkdlem4  26900  wlk2v2e  26917  3wlkdlem2  26920  3wlkdlem4  26922  3pthdlem1  26924  eupth0  26974  eupthp1  26976  eucrctshift  27003  eucrct2eupth  27005  extwwlkfablem1  27100  extwwlkfablem2  27102  numclwwlkovf2ex  27109  numclwlk2lem2f  27125  frgrregord013  27141  ex-exp  27195  ex-bc  27197  ex-gcd  27202  ex-lcm  27203  ex-ind-dvds  27206  smcnlem  27440  ipidsq  27453  dipcj  27457  dip0r  27460  nmlnoubi  27539  nmblolbii  27542  blocnilem  27547  ip1ilem  27569  ip2i  27571  ipdirilem  27572  ipasslem10  27582  ipasslem11  27583  siilem1  27594  hvmul0  27769  hvsubsub4i  27804  hvnegdii  27807  hvsubeq0i  27808  hvsubcan2i  27809  hvsubaddi  27811  hvsub0  27821  hisubcomi  27849  normlem0  27854  normlem1  27855  normlem2  27856  normlem3  27857  normlem9  27863  norm-ii-i  27882  norm3difi  27892  normpari  27899  polid2i  27902  polidi  27903  bcsiALT  27924  pjhthlem1  28138  chdmm3i  28226  chdmm4i  28227  chjidm  28267  chj4i  28270  chjjdiri  28271  spanunsni  28326  pjoml4i  28334  cmcm2i  28340  qlax4i  28377  qlax5i  28378  pjadjii  28421  pjmulii  28424  pjsubii  28425  pjssmii  28428  pjcji  28431  pjneli  28470  hoadd32i  28525  ho0subi  28542  hosubid1  28545  hosd2i  28570  hopncani  28571  hosubeq0i  28573  lnopeq0lem1  28752  lnopunilem1  28757  lnophmlem2  28764  nmbdoplbi  28771  nmcopexi  28774  lnfnmuli  28791  nmcfnexi  28798  nmoptri2i  28846  nmopcoadji  28848  golem1  29018  mdsl1i  29068  cvmdi  29071  mdslmd3i  29079  csmdsymi  29081  xrge00  29513  archirngz  29570  archiabllem2c  29576  gsumle  29606  gsummpt2co  29607  gsumvsca1  29609  gsumvsca2  29610  xrge0slmod  29671  psgnfzto1st  29682  lmat22det  29712  madjusmdetlem4  29720  raddcn  29799  xrge0iifhom  29807  xrge0mulc1cn  29811  cbvesum  29927  gsumesum  29944  esumpfinvallem  29959  esumpfinvalf  29961  dya2icoseg  30162  sitg0  30231  eulerpartlemd  30251  eulerpartlemgvv  30261  eulerpartlemgh  30263  fib0  30284  fib1  30285  fibp1  30286  orrvcval4  30349  orrvcoel  30350  orrvccel  30351  coinflipprob  30364  coinflippvt  30369  ballotlem2  30373  ballotth  30422  signstf0  30467  signstfvn  30468  signsvtn0  30469  signstfvp  30470  signstfveq0  30476  signsvf0  30479  signsvf1  30480  signsvfn  30481  signshf  30487  itgexpif  30493  brepr0  30500  subfacp1lem1  30922  subfacp1lem5  30927  subfacval2  30930  subfaclim  30931  subfacval3  30932  cvxpconn  30985  cvxsconn  30986  mrsub0  31174  problem4  31323  quad3  31325  sinccvglem  31327  iexpire  31382  faclimlem1  31390  frrlem5  31538  fwddifnp1  31967  knoppcnlem10  32187  knoppndvlem7  32204  knoppndvlem21  32218  cnndvlem1  32223  finxpreclem4  32902  ptrest  33079  poimirlem27  33107  dvtan  33131  itgabsnc  33150  ftc1anclem8  33163  dvasin  33167  dvacos  33168  areacirclem1  33171  areacirclem4  33174  areacirc  33176  prdstotbnd  33264  prdsbnd2  33265  repwsmet  33304  rrnequiv  33305  reheibor  33309  dalem-cly  34476  pmodN  34655  cdleme0cp  35020  cdleme0cq  35021  cdleme1  35033  cdleme3d  35037  cdleme3h  35041  cdleme4  35044  cdleme5  35046  cdleme7a  35049  cdleme8  35056  cdleme9  35059  cdleme10  35060  cdleme11g  35071  cdleme15b  35081  cdleme21  35144  cdleme22e  35151  cdleme22eALTN  35152  cdleme23c  35158  cdleme25cv  35165  cdleme35b  35257  cdleme35c  35258  cdleme42a  35278  cdleme42d  35280  cdleme43aN  35296  cdlemeg46gfv  35337  cdlemk35  35719  dihjatcclem1  36226  lcdval2  36398  mapdpglem21  36500  mapfzcons  36798  mapfzcons1cl  36800  2rexfrabdioph  36879  3rexfrabdioph  36880  4rexfrabdioph  36881  6rexfrabdioph  36882  7rexfrabdioph  36883  rabdiophlem2  36885  diophren  36896  rabren3dioph  36898  pellexlem5  36916  pell1qr1  36954  rmspecfund  36993  jm2.17a  37046  jm2.17b  37047  jm2.27c  37093  jm2.27dlem5  37099  lmhmlnmsplit  37176  arearect  37321  areaquad  37322  relexp2  37489  trclfvdecomr  37540  k0004val0  37973  inductionexd  37974  unitadd  38019  amgm2d  38022  amgm3d  38023  lhe4.4ex1a  38049  expgrowthi  38053  expgrowth  38055  bccn1  38064  binomcxplemdvbinom  38073  binomcxplemdvsum  38075  binomcxplemnotnn0  38076  binomcxp  38077  refsumcn  38711  unirnmapsn  38915  oddfl  38988  infleinflem2  39086  sumnnodd  39298  cosnegpi  39413  dvcosre  39461  dvsinax  39463  ioodvbdlimc1lem2  39484  ioodvbdlimc2lem  39486  dvmptmulf  39489  dvxpaek  39492  dvmptfprod  39497  dvnprodlem2  39499  dvnprodlem3  39500  itgsin0pilem1  39502  itgsinexplem1  39506  itgsubsticclem  39528  stoweidlem13  39567  wallispilem4  39622  wallispi2lem1  39625  wallispi2lem2  39626  stirlinglem1  39628  dirkerper  39650  dirkertrigeqlem1  39652  dirkertrigeqlem3  39654  dirkertrigeq  39655  dirkeritg  39656  dirkercncflem1  39657  dirkercncflem2  39658  fourierdlem36  39697  fourierdlem41  39702  fourierdlem42  39703  fourierdlem48  39708  fourierdlem56  39716  fourierdlem57  39717  fourierdlem58  39718  fourierdlem60  39720  fourierdlem61  39721  fourierdlem62  39722  fourierdlem65  39725  fourierdlem73  39733  fourierdlem80  39740  fourierdlem87  39747  fourierdlem89  39749  fourierdlem90  39750  fourierdlem91  39751  fourierdlem100  39760  fourierdlem103  39763  fourierdlem107  39767  fourierdlem112  39772  fourierdlem113  39773  fourierdlem115  39775  fouriercnp  39780  sqwvfoura  39782  sqwvfourb  39783  fourierswlem  39784  fouriersw  39785  etransclem2  39790  etransclem37  39825  etransclem46  39834  hoidmvlelem3  40148  vonioolem2  40232  issmflem  40273  smfmullem2  40336  1t10e1p1e11  40646  1t10e1p1e11OLD  40647  pfx1  40740  pfxccatpfx1  40756  pfxccatpfx2  40757  fmtno0  40781  fmtno1  40782  fmtnorec2lem  40783  fmtnorec3  40789  fmtno2  40791  fmtno3  40792  fmtno4  40793  fmtno4sqrt  40812  fmtno4prmfac  40813  2exp5  40836  139prmALT  40840  31prm  40841  2exp7  40843  2exp11  40846  mod42tp1mod8  40848  lighneallem2  40852  5tcu2e40  40861  3exp4mod41  40862  41prothprmlem1  40863  41prothprmlem2  40864  41prothprm  40865  bits0ALTV  40919  nnsum3primes4  40995  nnsum3primesgbe  40999  nnsum4primesodd  41003  nnsum4primesoddALTV  41004  nnsum4primeseven  41007  nnsum4primesevenALTV  41008  bgoldbtbndlem1  41012  tgoldbachlt  41021  tgoldbachltOLD  41028  2t6m3t4e0  41444  zlmodzxzequa  41603  zlmodzxznm  41604  zlmodzxzequap  41606  nn0sumshdiglemA  41735  nn0sumshdiglemB  41736  nn0sumshdiglem1  41737  sec0  41824  dfdp2OLD  41831  amgmw2d  41883
  Copyright terms: Public domain W3C validator