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

Theorem oveq2i 6374
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 6371 . 2 (𝐴 = 𝐵 → (𝐶𝐹𝐴) = (𝐶𝐹𝐵))
31, 2ax-mp 5 1 (𝐶𝐹𝐴) = (𝐶𝐹𝐵)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1468  (class class class)co 6363
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1698  ax-4 1711  ax-5 1789  ax-6 1836  ax-7 1883  ax-10 1965  ax-11 1970  ax-12 1983  ax-13 2137  ax-ext 2485
This theorem depends on definitions:  df-bi 192  df-or 379  df-an 380  df-3an 1023  df-tru 1471  df-ex 1693  df-nf 1697  df-sb 1829  df-clab 2492  df-cleq 2498  df-clel 2501  df-nfc 2635  df-rex 2797  df-rab 2800  df-v 3068  df-dif 3429  df-un 3431  df-in 3433  df-ss 3440  df-nul 3758  df-if 3909  df-sn 3996  df-pr 3998  df-op 4002  df-uni 4229  df-br 4435  df-iota 5597  df-fv 5641  df-ov 6366
This theorem is referenced by:  caov32  6571  caov4  6575  caov42  6577  seqomsuc  7251  oa1suc  7310  om1  7320  oe1  7322  oawordeulem  7332  oeoalem  7374  nnm1  7426  nnm2  7427  nneob  7430  omopthlem1  7433  mapsnconst  7600  mapsncnv  7601  map2xp  7826  cantnflt  8262  cnfcom2  8292  infxpenc  8534  infxpenc2  8538  ackbij1lem5  8739  alephom  9095  pwxpndom2  9175  adderpqlem  9464  addassnq  9468  mulcanenq  9470  distrnq  9471  ltanq  9481  ltexnq  9485  halfnq  9486  ltrnq  9489  archnq  9490  addclprlem2  9527  prlem934  9543  prlem936  9557  addcmpblnr  9578  mulcmpblnrlem  9579  ltsrpr  9586  m1p1sr  9601  m1m1sr  9602  0idsr  9606  1idsr  9607  00sr  9608  pn0sr  9610  recexsrlem  9612  mulgt0sr  9614  sqgt0sr  9615  mulresr  9648  axmulcom  9664  axmulass  9666  axdistr  9667  axi2m1  9668  ax1rid  9670  axcnre  9673  mul02lem1  9894  addid1  9898  negid  10008  negsub  10009  subneg  10010  negsubdii  10046  muleqadd  10345  crne0  10691  2p2e4  10817  3p2e5  10832  3p3e6  10833  4p2e6  10834  4p3e7  10835  4p4e8  10836  5p2e7  10837  5p3e8  10838  5p4e9  10839  5p5e10  10840  6p2e8  10841  6p3e9  10842  6p4e10  10843  7p2e9  10844  7p3e10  10845  8p2e10  10846  3t3e9  10852  8th4div3  10923  halfpm6th  10924  addltmul  10938  nn0n0n1ge2  11023  nneo  11109  zeo  11111  numsuc  11153  numltc  11161  numsucc  11167  numma  11172  nummul1c  11177  6p5lem  11190  4t3lem  11212  decbin2  11245  xmulmnf1  11657  fztp  11950  fzprval  11954  fztpval  11955  fzshftral  11980  fz0tp  11992  fz0to3un2pr  11993  fzo01  12099  fzo12sn  12100  fzo13pr  12101  fzo0to2pr  12102  fzo0to3tp  12103  fzo0to42pr  12104  quoremz  12190  quoremnn0ALT  12192  intfrac2  12193  intfracq  12194  sqval  12448  sqrecii  12471  cu2  12487  i3  12490  i4  12491  binom2i  12498  binom3  12507  crreczi  12511  nn0opthlem1  12568  facp1  12578  faclbnd  12589  faclbnd2  12590  faclbnd4lem1  12592  faclbnd4lem4  12595  bcn1  12612  bcn2  12618  4bc3eq4  12627  4bc2eq6  12628  hashgadd  12674  hashxplem  12725  hashmap  12727  hashfun  12729  hashbclem  12738  fz1isolem  12747  ccatlid  12861  ccatrid  12862  ccats1val2  12894  ccat2s1p2  12896  wrdeqs1cat  12964  swrdccatin12lem3  12979  swrdccat3a  12983  cats1fvn  13092  cats1cat  13095  cats2cat  13096  s3fn  13144  swrds2  13171  reim0  13341  cji  13382  sqrtm1  13499  absi  13509  rddif  13563  iseraltlem2  13909  iseralt  13911  fsump1i  13990  fsummulc2  14005  incexclem  14054  incexc  14055  arisum2  14079  geoihalfsum  14098  mertenslem1  14100  mertens  14102  risefall0lem  14239  risefac1  14246  fallfac1  14247  fallfacfwd  14249  bpoly0  14263  bpoly1  14264  bpolydiflem  14267  bpoly2  14270  bpoly3  14271  bpoly4  14272  fsumcube  14273  ef0lem  14293  ege2le3  14304  eft0val  14326  ef4p  14327  efgt1p2  14328  efgt1p  14329  tanval2  14347  efival  14366  ef01bndlem  14398  sin01bnd  14399  cos01bnd  14400  cos1bnd  14401  cos2bnd  14402  rpnnen2lem11  14437  sqr2irrlem  14460  odd2np1lem  14525  odd2np1  14526  oddp1even  14528  divalglem5OLD  14538  divalglem5  14539  divalglem6  14540  bits0  14563  0bits  14575  gcdaddmlem  14654  6gcd4e2  14664  lcmneg  14730  3lcm2e6woprm  14742  6lcm4e12  14743  3prm  14803  3lcm2e6  14843  phiprm  14887  eulerthlem2  14892  prmdiv  14895  opoe  14923  pythagtriplem12  14938  pythagtriplem14  14940  pcmpt  14999  pcfac  15006  prmpwdvds  15010  pockthi  15013  prmreclem2  15023  prmreclem6  15027  4sqlem5  15048  4sqlem13OLD  15063  4sqlem13  15069  modxai  15202  mod2xnegi  15205  gcdi  15207  decexp2  15209  numexpp1  15212  numexp2x  15213  decsplit0b  15214  decsplit1  15216  decsplit  15217  2exp16  15222  prmlem0  15238  139prm  15256  163prm  15257  317prm  15258  631prm  15259  1259lem1  15263  1259lem3  15265  1259lem4  15266  1259lem5  15267  1259prm  15268  2503lem1  15269  2503lem2  15270  2503lem3  15271  2503prm  15272  4001lem1  15273  4001lem2  15274  4001lem3  15275  4001lem4  15276  ressinbas  15350  rcaninv  15865  rescfth  16008  xpccatid  16239  oduval  16541  oppgmnd  17166  psgnunilem2  17297  psgnunilem4  17299  psgnpmtr  17312  psgn0fv0  17313  psgnsn  17322  psgnprfval1  17324  lsmmod2  17487  efgi0  17531  efgi1  17532  efginvrel2  17538  efgsval2  17544  efgsp1  17548  efgredleme  17554  efgredlemc  17556  efgcpbllemb  17566  frgpnabllem1  17670  lt6abl  17690  gsumconstf  17729  gsum2dlem2  17764  pwsgsum  17772  fsfnn0gsumfsffz  17773  dprd0  17824  dprdf1  17826  dprd2da  17835  ablfac1lem  17861  pgpfac1lem3  17870  pgpfaclem1  17874  srgbinomlem4  17936  opprring  18019  mulgass3  18025  evlsval  18901  mpff  18915  ply1assa  18951  gsumply1subr  18986  ply1coe  19048  coe1fzgsumdlem  19053  coe1fzgsumd  19054  gsumply1eq  19057  evl1gsumdlem  19102  evl1gsumd  19103  xrsnsgrp  19162  znbas  19272  znzrh2  19274  dsmmval2  19457  frlmip  19494  matgsum  19620  madetsumid  19644  mdetrsca  19786  mdetrsca2  19787  mdettpos  19794  m2detleiblem2  19811  madugsum  19826  madurid  19827  cpmat  19891  pmatcollpwfi  19964  pmatcollpw3fi1lem1  19968  pm2mpval  19977  mp2pm2mplem5  19992  chpmat1dlem  20017  chpmat1d  20018  chpidmat  20029  cpmidpmat  20055  cpmadugsumfi  20059  chcoeffeqlem  20067  cayleyhamilton0  20071  cayleyhamiltonALT  20073  cayleyhamilton1  20074  restin  20339  imacmp  20569  concompcon  20604  uptx  20797  cnpflf2  21173  tmdgsum2  21269  tsmsres  21316  tsmsf1o  21317  tsmsmhm  21318  prdsxmet  21542  resspwsds  21545  prdsxmslem2  21702  metdcn2  22015  metdcn  22016  metdscn2  22032  metdscn2OLD  22047  iimulcn  22124  icchmeo  22127  xrhmeo  22132  cnrehmeo  22139  cnheiborlem  22140  evth  22145  evth2  22146  lebnumlem2  22148  lebnumlem2OLD  22151  reparphti  22187  pcoass  22214  pi1xfrcnv  22247  ipcau2  22367  minveclem4  22533  minveclem4OLD  22545  pjthlem1  22550  ovolunlem1a  22608  unmbl  22650  uniioombl  22707  iblitg  22887  dfitg  22888  itg0  22898  iblcnlem1  22906  itgcnlem  22908  itgabs  22953  limcdif  22992  limccnp  23007  limccnp2  23008  dvexp  23068  dvmptid  23072  dvmptc  23073  dvmptfsum  23088  dveflem  23092  dvsincos  23094  mvth  23105  dvlipcn  23107  dvivthlem1  23121  dvfsumle  23134  dvfsumlem2  23140  itgsubst  23162  tdeglem4  23170  tdeglem2  23171  plypf1  23327  plymullem1  23329  coesub  23372  dgrmulc  23386  fta1lem  23421  vieta1lem1  23424  vieta1lem2  23425  aalioulem4  23452  aaliou3lem3  23461  abelthlem2  23548  abelthlem8  23555  abelthlem9  23556  sinhalfpilem  23579  efhalfpi  23587  cospi  23588  efipi  23589  sin2pi  23591  cos2pi  23592  ef2pi  23593  sin2pim  23601  cos2pim  23602  sinmpi  23603  cosmpi  23604  sinppi  23605  cosppi  23606  sincosq4sgn  23617  tangtx  23621  sincos4thpi  23629  sincos6thpi  23631  sincos3rdpi  23632  pige3  23633  abssinper  23634  efif1olem4  23655  efifo  23657  eff1o  23659  circgrp  23662  circsubm  23663  logneg  23698  logimul  23724  logneg2  23725  dvrelog  23743  logcnlem4  23751  dvlog  23757  dvlog2  23759  logtayl  23766  1cxp  23778  ecxp  23779  cxpsqrt  23809  dvsqrt  23843  dvcnsqrt  23845  root1eq1  23856  cxpeq  23858  elogb  23868  ang180lem1  23899  ang180lem2  23900  heron  23925  1cubrlem  23928  1cubr  23929  dcubic2  23931  mcubic  23934  cubic2  23935  binom4  23937  dquartlem1  23938  dquartlem2  23939  dquart  23940  quart1lem  23942  quart1  23943  quartlem1  23944  asinsin  23979  asin1  23981  acos1  23982  atanlogsublem  24002  atanlogsub  24003  efiatan2  24004  2efiatan  24005  tanatan  24006  atanbnd  24013  atan1  24015  dvatan  24022  atantayl2  24025  leibpilem2  24028  leibpi  24029  log2cnv  24031  log2tlbnd  24032  log2ublem1  24033  log2ublem2  24034  log2ublem3  24035  log2ub  24036  birthday  24041  amgmlem  24076  emcllem5  24086  lgamgulmlem2  24116  lgamgulmlem5  24119  lgam1  24150  wilthlem2  24155  ftalem6  24165  basellem2  24169  basellem3  24170  basellem5  24172  basellem8  24175  cht1  24253  chp1  24255  1sgmprm  24288  ppiublem2  24292  ppiub  24293  chtublem  24300  chtub  24301  logfacbnd3  24312  bcp1ctr  24368  bclbnd  24369  bposlem1  24373  bposlem4  24376  bposlem6  24378  bposlem8  24380  bposlem9  24381  lgslem1  24385  lgsdir2lem1  24412  lgsdir2lem2  24413  lgsdir2lem3  24414  lgsdir2lem5  24416  lgs1  24427  lgseisenlem1  24438  lgseisenlem3  24440  lgsquadlem1  24443  lgsquadlem2  24444  lgsquad2lem2  24448  m1lgs  24451  2sqlem8  24461  2sqblem  24466  logdivsum  24532  mulog2sumlem2  24534  log2sumbnd  24543  selberglem1  24544  selberglem2  24545  pntrmax  24563  pntibndlem2  24590  pntibndlem3  24591  pntlemg  24597  pntlemr  24601  pntlemo  24606  ostth2lem3  24634  ostth2lem4  24635  istrkg3ld  24670  trgcgrg  24721  tgcgr4  24737  colperpexlem1  24933  ax5seglem7  25126  axlowdimlem4  25136  axlowdimlem16  25148  0wlk  25436  0trl  25437  wlkntrllem2  25451  wlkntrl  25453  constr1trl  25479  1pthonlem1  25480  constr2wlk  25489  constr2trl  25490  wlkdvspthlem  25498  constr3trllem3  25541  constr3trllem4  25542  constr3trllem5  25543  constr3pthlem1  25544  constr3pthlem3  25546  clwwlkn2  25664  clwlkisclwwlk2  25679  wwlkext2clwwlk  25692  vdgr1c  25793  nbhashuvtx1  25803  vdegp1ai  25872  vdegp1bi  25873  vdegp1ci  25874  extwwlkfablem2  25966  numclwwlkovf2ex  25974  numclwlk2lem2f  25991  frgraregord013  26006  ex-ind-dvds  26060  smcnlem  26496  ipidsq  26512  dipcj  26516  dip0r  26519  nmlnoubi  26600  nmblolbii  26603  blocnilem  26608  ip1ilem  26630  ip2i  26632  ipdirilem  26633  ipasslem10  26643  ipasslem11  26644  siilem1  26655  hvmul0  26840  hvsubsub4i  26875  hvnegdii  26878  hvsubeq0i  26879  hvsubcan2i  26880  hvsubaddi  26882  hvsub0  26892  hisubcomi  26920  normlem0  26925  normlem1  26926  normlem2  26927  normlem3  26928  normlem9  26934  norm-ii-i  26953  norm3difi  26963  normpari  26970  polid2i  26973  polidi  26974  bcsiALT  26995  pjhthlem1  27207  chdmm3i  27295  chdmm4i  27296  chjidm  27336  chj4i  27339  chjjdiri  27340  spanunsni  27395  pjoml4i  27403  cmcm2i  27409  qlax4i  27446  qlax5i  27447  pjadjii  27490  pjmulii  27493  pjsubii  27494  pjssmii  27497  pjcji  27500  pjneli  27539  hoadd32i  27594  ho0subi  27611  hosubid1  27614  hosd2i  27639  hopncani  27640  hosubeq0i  27642  lnopeq0lem1  27821  lnopunilem1  27826  lnophmlem2  27833  nmbdoplbi  27840  nmcopexi  27843  lnfnmuli  27860  nmcfnexi  27867  nmoptri2i  27915  nmopcoadji  27917  golem1  28087  mdsl1i  28137  cvmdi  28140  mdslmd3i  28148  csmdsymi  28150  xrge00  28604  archirngz  28661  archiabllem2c  28667  gsumle  28697  gsummpt2co  28698  gsumvsca1  28700  gsumvsca2  28701  xrge0slmod  28762  psgnfzto1st  28773  lmat22det  28803  madjusmdetlem4  28811  raddcn  28890  xrge0iifhom  28898  xrge0mulc1cn  28902  cbvesum  29018  gsumesum  29035  esumpfinvallem  29050  esumpfinvalf  29052  dya2icoseg  29253  sitg0  29333  eulerpartlemd  29353  eulerpartlemgvv  29363  eulerpartlemgh  29365  fib0  29386  fib1  29387  fibp1  29388  orrvcval4  29451  orrvcoel  29452  orrvccel  29453  coinflipprob  29466  coinflippvt  29471  ballotlem2  29475  ballotth  29524  ballotthOLD  29562  signstf0  29610  signstfvn  29611  signsvtn0  29612  signstfvp  29613  signstfveq0  29619  signsvf0  29622  signsvf1  29623  signsvfn  29624  signshf  29630  subfacp1lem1  30054  subfacp1lem5  30059  subfacval2  30062  subfaclim  30063  subfacval3  30064  cvxpcon  30117  cvxscon  30118  mrsub0  30306  problem4  30452  quad3  30454  sinccvglem  30468  iexpire  30522  faclimlem1  30530  frrlem5  30669  fwddifnp1  31083  knoppcnlem10  31300  finxpreclem4  32007  ptrest  32177  poimirlem27  32205  dvtan  32230  itgabsnc  32249  ftc1anclem8  32262  dvasin  32266  dvacos  32267  areacirclem1  32270  areacirclem4  32273  areacirc  32275  prdstotbnd  32363  prdsbnd2  32364  repwsmet  32403  rrnequiv  32404  reheibor  32408  dalem-cly  33476  pmodN  33655  cdleme0cp  34020  cdleme0cq  34021  cdleme1  34033  cdleme3d  34037  cdleme3h  34041  cdleme4  34044  cdleme5  34046  cdleme7a  34049  cdleme8  34056  cdleme9  34059  cdleme10  34060  cdleme11g  34071  cdleme15b  34081  cdleme21  34144  cdleme22e  34151  cdleme22eALTN  34152  cdleme23c  34158  cdleme25cv  34165  cdleme35b  34257  cdleme35c  34258  cdleme42a  34278  cdleme42d  34280  cdleme43aN  34296  cdlemeg46gfv  34337  cdlemk35  34719  dihjatcclem1  35226  lcdval2  35398  mapdpglem21  35500  mapfzcons  35798  mapfzcons1cl  35800  2rexfrabdioph  35879  3rexfrabdioph  35880  4rexfrabdioph  35881  6rexfrabdioph  35882  7rexfrabdioph  35883  rabdiophlem2  35885  diophren  35896  rabren3dioph  35898  pellexlem5  35917  pell1qr1  35957  rmspecfund  35997  jm2.17a  36050  jm2.17b  36051  jm2.27c  36102  jm2.27dlem5  36108  lmhmlnmsplit  36185  arearect  36340  areaquad  36341  relexp2  36508  trclfvdecomr  36559  k0004val0  36950  inductionexd  36951  unitadd  36998  amgm2d  37006  amgm3d  37008  lhe4.4ex1a  37035  expgrowthi  37039  expgrowth  37041  bccn1  37050  binomcxplemdvbinom  37059  binomcxplemdvsum  37061  binomcxplemnotnn0  37062  binomcxp  37063  refsumcn  37699  unirnmapsn  37854  oddfl  37866  infleinflem2  37970  m1expevenOLD  38072  sumnnodd  38114  cosnegpi  38151  dvcosre  38200  dvsinax  38202  ioodvbdlimc1lem2  38223  ioodvbdlimc1lem2OLD  38225  ioodvbdlimc2lem  38227  ioodvbdlimc2lemOLD  38228  dvmptmulf  38231  dvxpaek  38234  dvmptfprod  38239  dvnprodlem2  38241  dvnprodlem3  38242  itgsin0pilem1  38245  itgsinexplem1  38249  itgsubsticclem  38271  stoweidlem13  38309  wallispilem4  38366  wallispi2lem1  38369  wallispi2lem2  38370  stirlinglem1  38372  dirkerper  38394  dirkertrigeqlem1  38396  dirkertrigeqlem3  38398  dirkertrigeq  38399  dirkeritg  38400  dirkercncflem1  38401  dirkercncflem2  38402  fourierdlem36  38442  fourierdlem41  38447  fourierdlem42  38448  fourierdlem42OLD  38449  fourierdlem48  38454  fourierdlem56  38462  fourierdlem57  38463  fourierdlem58  38464  fourierdlem60  38466  fourierdlem61  38467  fourierdlem62  38468  fourierdlem65  38471  fourierdlem73  38479  fourierdlem80  38486  fourierdlem87  38493  fourierdlem89  38495  fourierdlem90  38496  fourierdlem91  38497  fourierdlem100  38506  fourierdlem103  38509  fourierdlem107  38513  fourierdlem112  38518  fourierdlem113  38519  fourierdlem115  38521  fouriercnp  38526  sqwvfoura  38528  sqwvfourb  38529  fourierswlem  38530  fouriersw  38531  etransclem2  38537  etransclem37  38572  etransclem46  38581  hoidmvlelem3  38882  vonioolem2  38967  1t10e1p1e11  39230  deccarry  39235  bits0ALTV  39328  nnsum3primes4  39403  nnsum3primesgbe  39407  nnsum4primesodd  39411  nnsum4primesoddALTV  39412  nnsum4primeseven  39415  nnsum4primesevenALTV  39416  bgoldbtbndlem1  39420  tgoldbachlt  39429  5tcu2e40  39435  3exp4mod41  39436  41prothprmlem1  39437  41prothprmlem2  39438  41prothprm  39439  pfx1  39474  pfxccatpfx1  39490  pfxccatpfx2  39491  uhgrstrrepe  39704  vdegp1ci-av  40154  1wlkp1lem6  40287  1wlkp1lem8  40289  1wlkp1  40290  uhgr1wlkspthlem2  40360  pthdlem1  40372  pthdlem2  40374  pthd  40375  crctcsh1wlkn0lem4  40416  crctcsh1wlkn0lem5  40417  crctcsh1wlkn0lem6  40418  crctcshlem4  40423  crctcsh1wlkn0  40424  21wlkdlem2  40533  21wlkdlem4  40535  2pthdlem1  40537  clwlkclwwlk2  40612  wwlksext2clwwlk  40631  0ewlk  40682  1ewlk  40683  01wlk  40684  1pthdlem1  40702  1pthdlem2  40703  11wlkdlem1  40704  11wlkdlem4  40707  1wlk2v2e  40724  31wlkdlem2  40727  31wlkdlem4  40729  3pthdlem1  40731  eupth0  40782  eupthp1  40784  eucrctshift  40811  eucrct2eupth  40813  av-extwwlkfablem1  40908  av-extwwlkfablem2  40910  av-numclwwlkovf2ex  40917  av-numclwlk2lem2f  40933  av-frgraregord013  40949  2t6m3t4e0  41319  zlmodzxzequa  41479  zlmodzxznm  41480  zlmodzxzequap  41482  nn0sumshdiglemA  41619  nn0sumshdiglemB  41620  nn0sumshdiglem1  41621  sec0  41669
  Copyright terms: Public domain W3C validator