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

Theorem oveq2i 6326
Description: Equality inference for operation value. (Contributed by NM, 28-Feb-1995.)
Hypothesis
Ref Expression
oveq1i.1  |-  A  =  B
Assertion
Ref Expression
oveq2i  |-  ( C F A )  =  ( C F B )

Proof of Theorem oveq2i
StepHypRef Expression
1 oveq1i.1 . 2  |-  A  =  B
2 oveq2 6323 . 2  |-  ( A  =  B  ->  ( C F A )  =  ( C F B ) )
31, 2ax-mp 5 1  |-  ( C F A )  =  ( C F B )
Colors of variables: wff setvar class
Syntax hints:    = wceq 1455  (class class class)co 6315
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3an 993  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-rex 2755  df-rab 2758  df-v 3059  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-nul 3744  df-if 3894  df-sn 3981  df-pr 3983  df-op 3987  df-uni 4213  df-br 4417  df-iota 5565  df-fv 5609  df-ov 6318
This theorem is referenced by:  caov32  6523  caov4  6527  caov42  6529  seqomsuc  7200  oa1suc  7259  om1  7269  oe1  7271  oawordeulem  7281  oeoalem  7323  nnm1  7375  nnm2  7376  nneob  7379  omopthlem1  7382  mapsnconst  7543  mapsncnv  7544  map2xp  7768  cantnflt  8203  cnfcom2  8233  infxpenc  8475  infxpenc2  8479  ackbij1lem5  8680  alephom  9036  pwxpndom2  9116  adderpqlem  9405  addassnq  9409  mulcanenq  9411  distrnq  9412  ltanq  9422  ltexnq  9426  halfnq  9427  ltrnq  9430  archnq  9431  addclprlem2  9468  prlem934  9484  prlem936  9498  addcmpblnr  9519  mulcmpblnrlem  9520  ltsrpr  9527  m1p1sr  9542  m1m1sr  9543  0idsr  9547  1idsr  9548  00sr  9549  pn0sr  9551  recexsrlem  9553  mulgt0sr  9555  sqgt0sr  9556  mulresr  9589  axmulcom  9605  axmulass  9607  axdistr  9608  axi2m1  9609  ax1rid  9611  axcnre  9614  mul02lem1  9835  addid1  9839  add42iOLD  9881  negid  9947  negsub  9948  subneg  9949  negsubdii  9986  muleqadd  10284  crne0  10630  2p2e4  10756  3p2e5  10771  3p3e6  10772  4p2e6  10773  4p3e7  10774  4p4e8  10775  5p2e7  10776  5p3e8  10777  5p4e9  10778  5p5e10  10779  6p2e8  10780  6p3e9  10781  6p4e10  10782  7p2e9  10783  7p3e10  10784  8p2e10  10785  3t3e9  10791  8th4div3  10862  halfpm6th  10863  addltmul  10877  nn0n0n1ge2  10961  nneo  11048  zeo  11050  numsuc  11092  numltc  11100  numsucc  11106  numma  11111  nummul1c  11116  6p5lem  11129  4t3lem  11151  decbin2  11184  xmulmnf1  11591  fztp  11881  fzprval  11885  fztpval  11886  fzshftral  11911  fz0tp  11922  fz0to3un2pr  11923  fzo01  12026  fzo12sn  12027  fzo13pr  12028  fzo0to2pr  12029  fzo0to3tp  12030  fzo0to42pr  12031  quoremz  12114  quoremnn0ALT  12116  intfrac2  12117  intfracq  12118  sqval  12366  sqrecii  12389  cu2  12405  i3  12408  i4  12409  binom2i  12416  binom3  12425  crreczi  12429  nn0opthlem1  12486  facp1  12496  faclbnd  12507  faclbnd2  12508  faclbnd4lem1  12510  faclbnd4lem4  12513  bcn1  12530  bcn2  12536  4bc3eq4  12545  4bc2eq6  12546  hashgadd  12588  hashxplem  12638  hashmap  12640  hashfun  12642  hashbclem  12648  fz1isolem  12657  ccatlid  12766  ccatrid  12767  ccats1val2  12797  ccat2s1p2  12799  wrdeqs1cat  12868  swrdccatin12lem3  12883  swrdccat3a  12887  cats1fvn  12991  cats1cat  12994  s3fn  13042  swrds2  13066  reim0  13230  cji  13271  sqrtm1  13388  absi  13398  rddif  13452  iseraltlem2  13798  iseralt  13800  fsump1i  13879  fsummulc2  13894  incexclem  13943  incexc  13944  arisum2  13968  geoihalfsum  13987  mertenslem1  13989  mertens  13991  risefall0lem  14128  risefac1  14135  fallfac1  14136  fallfacfwd  14138  bpoly0  14152  bpoly1  14153  bpolydiflem  14156  bpoly2  14159  bpoly3  14160  bpoly4  14161  fsumcube  14162  ef0lem  14182  ege2le3  14193  eft0val  14215  ef4p  14216  efgt1p2  14217  efgt1p  14218  tanval2  14236  efival  14255  ef01bndlem  14287  sin01bnd  14288  cos01bnd  14289  cos1bnd  14290  cos2bnd  14291  rpnnen2lem11  14326  sqr2irrlem  14349  odd2np1lem  14413  odd2np1  14414  oddp1even  14416  divalglem5OLD  14425  divalglem5  14426  divalglem6  14427  bits0  14450  0bits  14462  gcdaddmlem  14541  6gcd4e2  14551  lcmneg  14617  3lcm2e6woprm  14629  6lcm4e12  14630  3prm  14690  3lcm2e6  14730  phiprm  14774  eulerthlem2  14779  prmdiv  14782  opoe  14810  pythagtriplem12  14825  pythagtriplem14  14827  pcmpt  14886  pcfac  14893  prmpwdvds  14897  pockthi  14900  prmreclem2  14910  prmreclem6  14914  4sqlem5  14935  4sqlem13OLD  14950  4sqlem13  14956  modxai  15089  mod2xnegi  15092  gcdi  15094  decexp2  15096  numexpp1  15099  numexp2x  15100  decsplit0b  15101  decsplit1  15103  decsplit  15104  2exp6OLD  15108  2exp16  15110  prmlem0  15126  139prm  15144  163prm  15145  317prm  15146  631prm  15147  1259lem1  15151  1259lem3  15153  1259lem4  15154  1259lem5  15155  1259prm  15156  2503lem1  15157  2503lem2  15158  2503lem3  15159  2503prm  15160  4001lem1  15161  4001lem2  15162  4001lem3  15163  4001lem4  15164  ressinbas  15234  rcaninv  15748  rescfth  15891  xpccatid  16122  oduval  16425  oppgmnd  17054  psgnunilem2  17185  psgnunilem4  17187  psgnpmtr  17200  psgn0fv0  17201  psgnsn  17210  psgnprfval1  17212  lsmmod2  17375  efgi0  17419  efgi1  17420  efginvrel2  17426  efgsval2  17432  efgsp1  17436  efgredleme  17442  efgredlemc  17444  efgcpbllemb  17454  frgpnabllem1  17558  lt6abl  17578  gsumconstf  17617  gsum2dlem2  17652  pwsgsum  17660  fsfnn0gsumfsffz  17661  dprd0  17713  dprdf1  17715  dprd2da  17724  ablfac1lem  17750  pgpfac1lem3  17759  pgpfaclem1  17763  srgbinomlem4  17825  opprring  17908  mulgass3  17914  evlsval  18791  mpff  18805  ply1assa  18841  gsumply1subr  18876  ply1coe  18938  ply1coeOLD  18939  coe1fzgsumdlem  18944  coe1fzgsumd  18945  gsumply1eq  18948  evl1gsumdlem  18993  evl1gsumd  18994  xrsnsgrp  19053  znbas  19163  znzrh2  19165  dsmmval2  19348  frlmip  19385  matgsum  19511  madetsumid  19535  mdetrsca  19677  mdetrsca2  19678  mdettpos  19685  m2detleiblem2  19702  madugsum  19717  madurid  19718  cpmat  19782  pmatcollpwfi  19855  pmatcollpw3fi1lem1  19859  pm2mpval  19868  mp2pm2mplem5  19883  chpmat1dlem  19908  chpmat1d  19909  chpidmat  19920  cpmidpmat  19946  cpmadugsumfi  19950  chcoeffeqlem  19958  cayleyhamilton0  19962  cayleyhamiltonALT  19964  cayleyhamilton1  19965  restin  20231  imacmp  20461  concompcon  20496  uptx  20689  cnpflf2  21064  tmdgsum2  21160  tsmsres  21207  tsmsf1o  21208  tsmsmhm  21209  prdsxmet  21433  resspwsds  21436  prdsxmslem2  21593  metdcn2  21906  metdcn  21907  metdscn2  21923  metdscn2OLD  21938  iimulcn  22015  icchmeo  22018  xrhmeo  22023  cnrehmeo  22030  cnheiborlem  22031  evth  22036  evth2  22037  lebnumlem2  22039  lebnumlem2OLD  22042  reparphti  22077  pcoass  22104  pi1xfrcnv  22137  ipcau2  22257  minveclem4  22423  minveclem4OLD  22435  pjthlem1  22440  ovolunlem1a  22498  unmbl  22540  uniioombl  22596  iblitg  22775  dfitg  22776  itg0  22786  iblcnlem1  22794  itgcnlem  22796  itgabs  22841  limcdif  22880  limccnp  22895  limccnp2  22896  dvexp  22956  dvmptid  22960  dvmptc  22961  dvmptfsum  22976  dveflem  22980  dvsincos  22982  mvth  22993  dvlipcn  22995  dvivthlem1  23009  dvfsumle  23022  dvfsumlem2  23028  itgsubst  23050  tdeglem4  23058  tdeglem2  23059  plypf1  23215  plymullem1  23217  coesub  23260  dgrmulc  23274  fta1lem  23309  vieta1lem1  23312  vieta1lem2  23313  aalioulem4  23340  aaliou3lem3  23349  abelthlem2  23436  abelthlem8  23443  abelthlem9  23444  sinhalfpilem  23467  efhalfpi  23475  cospi  23476  efipi  23477  sin2pi  23479  cos2pi  23480  ef2pi  23481  sin2pim  23489  cos2pim  23490  sinmpi  23491  cosmpi  23492  sinppi  23493  cosppi  23494  sincosq4sgn  23505  tangtx  23509  sincos4thpi  23517  sincos6thpi  23519  sincos3rdpi  23520  pige3  23521  abssinper  23522  efif1olem4  23543  efifo  23545  eff1o  23547  circgrp  23550  circsubm  23551  logneg  23586  logimul  23612  logneg2  23613  dvrelog  23631  logcnlem4  23639  dvlog  23645  dvlog2  23647  logtayl  23654  1cxp  23666  ecxp  23667  cxpsqrt  23697  dvsqrt  23731  dvcnsqrt  23733  root1eq1  23744  cxpeq  23746  elogb  23756  ang180lem1  23787  ang180lem2  23788  heron  23813  1cubrlem  23816  1cubr  23817  dcubic2  23819  mcubic  23822  cubic2  23823  binom4  23825  dquartlem1  23826  dquartlem2  23827  dquart  23828  quart1lem  23830  quart1  23831  quartlem1  23832  asinsin  23867  asin1  23869  acos1  23870  atanlogsublem  23890  atanlogsub  23891  efiatan2  23892  2efiatan  23893  tanatan  23894  atanbnd  23901  atan1  23903  dvatan  23910  atantayl2  23913  leibpilem2  23916  leibpi  23917  log2cnv  23919  log2tlbnd  23920  log2ublem1  23921  log2ublem2  23922  log2ublem3  23923  log2ub  23924  birthday  23929  amgmlem  23964  emcllem5  23974  lgamgulmlem2  24004  lgamgulmlem5  24007  lgam1  24038  wilthlem2  24043  ftalem6  24053  basellem2  24057  basellem3  24058  basellem5  24060  basellem8  24063  cht1  24141  chp1  24143  1sgmprm  24176  ppiublem2  24180  ppiub  24181  chtublem  24188  chtub  24189  logfacbnd3  24200  bcp1ctr  24256  bclbnd  24257  bposlem1  24261  bposlem4  24264  bposlem6  24266  bposlem8  24268  bposlem9  24269  lgslem1  24273  lgsdir2lem1  24300  lgsdir2lem2  24301  lgsdir2lem3  24302  lgsdir2lem5  24304  lgs1  24315  lgseisenlem1  24326  lgseisenlem3  24328  lgsquadlem1  24331  lgsquadlem2  24332  lgsquad2lem2  24336  m1lgs  24339  2sqlem8  24349  2sqblem  24354  logdivsum  24420  mulog2sumlem2  24422  log2sumbnd  24431  selberglem1  24432  selberglem2  24433  pntrmax  24451  pntibndlem2  24478  pntibndlem3  24479  pntlemg  24485  pntlemr  24489  pntlemo  24494  ostth2lem3  24522  ostth2lem4  24523  istrkg3ld  24558  trgcgrg  24609  tgcgr4  24625  colperpexlem1  24821  ax5seglem7  25014  axlowdimlem4  25024  axlowdimlem16  25036  0wlk  25324  0trl  25325  wlkntrllem2  25339  wlkntrl  25341  constr1trl  25367  1pthonlem1  25368  constr2wlk  25377  constr2trl  25378  wlkdvspthlem  25386  constr3trllem3  25429  constr3trllem4  25430  constr3trllem5  25431  constr3pthlem1  25432  constr3pthlem3  25434  clwwlkn2  25552  clwlkisclwwlk2  25567  wwlkext2clwwlk  25580  vdgr1c  25682  nbhashuvtx1  25692  vdegp1ai  25761  vdegp1bi  25762  vdegp1ci  25763  extwwlkfablem2  25855  numclwwlkovf2ex  25863  numclwlk2lem2f  25880  frgraregord013  25895  ex-ind-dvds  25948  smcnlem  26382  ipidsq  26398  dipcj  26402  dip0r  26405  nmlnoubi  26486  nmblolbii  26489  blocnilem  26494  ip1ilem  26516  ip2i  26518  ipdirilem  26519  ipasslem10  26529  ipasslem11  26530  siilem1  26541  hvmul0  26726  hvsubsub4i  26761  hvnegdii  26764  hvsubeq0i  26765  hvsubcan2i  26766  hvsubaddi  26768  hvsub0  26778  hisubcomi  26806  normlem0  26811  normlem1  26812  normlem2  26813  normlem3  26814  normlem9  26820  norm-ii-i  26839  norm3difi  26849  normpari  26856  polid2i  26859  polidi  26860  bcsiALT  26881  pjhthlem1  27093  chdmm3i  27181  chdmm4i  27182  chjidm  27222  chj4i  27225  chjjdiri  27226  spanunsni  27281  pjoml4i  27289  cmcm2i  27295  qlax4i  27332  qlax5i  27333  pjadjii  27376  pjmulii  27379  pjsubii  27380  pjssmii  27383  pjcji  27386  pjneli  27425  hoadd32i  27480  ho0subi  27497  hosubid1  27500  hosd2i  27525  hopncani  27526  hosubeq0i  27528  lnopeq0lem1  27707  lnopunilem1  27712  lnophmlem2  27719  nmbdoplbi  27726  nmcopexi  27729  lnfnmuli  27746  nmcfnexi  27753  nmoptri2i  27801  nmopcoadji  27803  golem1  27973  mdsl1i  28023  cvmdi  28026  mdslmd3i  28034  csmdsymi  28036  xrge00  28497  archirngz  28555  archiabllem2c  28561  gsumle  28591  gsummpt2co  28592  gsumvsca1  28594  gsumvsca2  28595  xrge0slmod  28656  psgnfzto1st  28667  lmat22det  28697  madjusmdetlem4  28705  raddcn  28784  xrge0iifhom  28792  xrge0mulc1cn  28796  cbvesum  28912  gsumesum  28929  esumpfinvallem  28944  esumpfinvalf  28946  dya2icoseg  29148  sitg0  29228  eulerpartlemd  29248  eulerpartlemgvv  29258  eulerpartlemgh  29260  fib0  29281  fib1  29282  fibp1  29283  orrvcval4  29346  orrvcoel  29347  orrvccel  29348  coinflipprob  29361  coinflippvt  29366  ballotlem2  29370  ballotth  29419  ballotthOLD  29457  signstf0  29506  signstfvn  29507  signsvtn0  29508  signstfvp  29509  signstfveq0  29515  signsvf0  29518  signsvf1  29519  signsvfn  29520  signshf  29526  subfacp1lem1  29951  subfacp1lem5  29956  subfacval2  29959  subfaclim  29960  subfacval3  29961  cvxpcon  30014  cvxscon  30015  mrsub0  30203  problem4  30349  quad3  30351  sinccvglem  30365  iexpire  30420  faclimlem1  30428  frrlem5  30567  fwddifnp1  30981  finxpreclem4  31831  ptrest  31984  poimirlem25  32010  poimirlem27  32012  dvtan  32037  itgabsnc  32056  ftc1anclem8  32069  dvasin  32073  dvacos  32074  areacirclem1  32077  areacirclem4  32080  areacirc  32082  prdstotbnd  32171  prdsbnd2  32172  repwsmet  32211  rrnequiv  32212  reheibor  32216  dalem-cly  33281  pmodN  33460  cdleme0cp  33825  cdleme0cq  33826  cdleme1  33838  cdleme3d  33842  cdleme3h  33846  cdleme4  33849  cdleme5  33851  cdleme7a  33854  cdleme8  33861  cdleme9  33864  cdleme10  33865  cdleme11g  33876  cdleme15b  33886  cdleme21  33949  cdleme22e  33956  cdleme22eALTN  33957  cdleme23c  33963  cdleme25cv  33970  cdleme35b  34062  cdleme35c  34063  cdleme42a  34083  cdleme42d  34085  cdleme43aN  34101  cdlemeg46gfv  34142  cdlemk35  34524  dihjatcclem1  35031  lcdval2  35203  mapdpglem21  35305  mapfzcons  35603  mapfzcons1cl  35605  2rexfrabdioph  35684  3rexfrabdioph  35685  4rexfrabdioph  35686  6rexfrabdioph  35687  7rexfrabdioph  35688  rabdiophlem2  35690  diophren  35701  rabren3dioph  35703  pellexlem5  35722  pell1qr1  35762  rmspecfund  35802  jm2.17a  35855  jm2.17b  35856  jm2.27c  35907  jm2.27dlem5  35913  lmhmlnmsplit  35990  arearect  36145  areaquad  36146  relexp2  36314  trclfvdecomr  36365  inductionexd  36638  unitadd  36686  amgm2d  36694  amgm3d  36695  lhe4.4ex1a  36722  expgrowthi  36726  expgrowth  36728  bccn1  36737  binomcxplemdvbinom  36746  binomcxplemdvsum  36748  binomcxplemnotnn0  36749  binomcxp  36750  refsumcn  37391  oddfl  37525  m1expevenOLD  37708  sumnnodd  37748  cosnegpi  37780  dvcosre  37819  dvsinax  37821  ioodvbdlimc1lem2  37842  ioodvbdlimc1lem2OLD  37844  ioodvbdlimc2lem  37846  ioodvbdlimc2lemOLD  37847  dvmptmulf  37850  dvxpaek  37853  dvmptfprod  37858  dvnprodlem2  37860  dvnprodlem3  37861  itgsin0pilem1  37864  itgsinexplem1  37868  itgsubsticclem  37890  stoweidlem13  37911  wallispilem4  37968  wallispi2lem1  37971  wallispi2lem2  37972  stirlinglem1  37974  dirkerper  37996  dirkertrigeqlem1  37998  dirkertrigeqlem3  38000  dirkertrigeq  38001  dirkeritg  38002  dirkercncflem1  38003  dirkercncflem2  38004  fourierdlem36  38044  fourierdlem41  38049  fourierdlem42  38050  fourierdlem42OLD  38051  fourierdlem48  38056  fourierdlem56  38064  fourierdlem57  38065  fourierdlem58  38066  fourierdlem60  38068  fourierdlem61  38069  fourierdlem62  38070  fourierdlem65  38073  fourierdlem73  38081  fourierdlem80  38088  fourierdlem87  38095  fourierdlem89  38097  fourierdlem90  38098  fourierdlem91  38099  fourierdlem100  38108  fourierdlem103  38111  fourierdlem107  38115  fourierdlem112  38120  fourierdlem113  38121  fourierdlem115  38123  fouriercnp  38128  sqwvfoura  38130  sqwvfourb  38131  fourierswlem  38132  fouriersw  38133  etransclem2  38139  etransclem37  38174  etransclem46  38183  hoidmvlelem3  38457  1t10e1p1e11  38748  deccarry  38753  bits0ALTV  38846  nnsum3primes4  38921  nnsum3primesgbe  38925  nnsum4primesodd  38929  nnsum4primesoddALTV  38930  nnsum4primeseven  38933  nnsum4primesevenALTV  38934  bgoldbtbndlem1  38938  tgoldbachlt  38947  5tcu2e40  38953  3exp4mod41  38954  41prothprmlem1  38955  41prothprmlem2  38956  41prothprm  38957  pfx1  38992  pfxccatpfx1  39008  pfxccatpfx2  39009  uhgr1wlkspthlem2  39786  pthdlem1  39792  pthdlem2  39794  pthd  39795  0ewlk  39828  1ewlk  39829  01wlk  39832  1pthdlem1  39850  1pthdlem2  39851  11wlkdlem1  39852  11wlkdlem4  39855  1wlk2v2e  39872  21wlkdlem2  39875  21wlkdlem4  39877  2pthdlem1  39879  31wlkdlem2  39901  31wlkdlem4  39903  3pthdlem1  39905  uhgrepe  39963  2t6m3t4e0  40402  zlmodzxzequa  40562  zlmodzxznm  40563  zlmodzxzequap  40565  nn0sumshdiglemA  40703  nn0sumshdiglemB  40704  nn0sumshdiglem1  40705  sec0  40753
  Copyright terms: Public domain W3C validator