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

Theorem oveq2i 6292
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 6289 . 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 1383  (class class class)co 6281
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 976  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-rex 2799  df-rab 2802  df-v 3097  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3771  df-if 3927  df-sn 4015  df-pr 4017  df-op 4021  df-uni 4235  df-br 4438  df-iota 5541  df-fv 5586  df-ov 6284
This theorem is referenced by:  caov32  6487  caov4  6491  caov42  6493  seqomsuc  7124  oa1suc  7183  om1  7193  oe1  7195  oawordeulem  7205  oeoalem  7247  nnm1  7299  nnm2  7300  nneob  7303  omopthlem1  7306  mapsnconst  7466  mapsncnv  7467  map2xp  7689  cantnflt  8094  cantnfltOLD  8124  cnfcom2  8149  cnfcom2OLD  8157  infxpenc  8398  infxpenc2  8402  infxpencOLD  8403  infxpenc2OLD  8406  ackbij1lem5  8607  alephom  8963  pwxpndom2  9046  adderpqlem  9335  addassnq  9339  mulcanenq  9341  distrnq  9342  ltanq  9352  ltexnq  9356  halfnq  9357  ltrnq  9360  archnq  9361  addclprlem2  9398  prlem934  9414  prlem936  9428  addcmpblnr  9449  mulcmpblnrlem  9450  ltsrpr  9457  m1p1sr  9472  m1m1sr  9473  0idsr  9477  1idsr  9478  00sr  9479  pn0sr  9481  recexsrlem  9483  mulgt0sr  9485  sqgt0sr  9486  mulresr  9519  axmulcom  9535  axmulass  9537  axdistr  9538  axi2m1  9539  ax1rid  9541  axcnre  9544  mul02lem1  9759  addid1  9763  add42iOLD  9805  negid  9871  negsub  9872  subneg  9873  negsubdii  9910  muleqadd  10200  crne0  10536  2p2e4  10660  3p2e5  10675  3p3e6  10676  4p2e6  10677  4p3e7  10678  4p4e8  10679  5p2e7  10680  5p3e8  10681  5p4e9  10682  5p5e10  10683  6p2e8  10684  6p3e9  10685  6p4e10  10686  7p2e9  10687  7p3e10  10688  8p2e10  10689  3t3e9  10695  8th4div3  10766  halfpm6th  10767  addltmul  10781  nn0n0n1ge2  10866  nneo  10953  zeo  10955  numsuc  10998  numltc  11006  numsucc  11012  numma  11017  nummul1c  11022  6p5lem  11035  4t3lem  11057  decbin2  11090  xmulmnf1  11479  fztp  11747  fzprval  11751  fztpval  11752  fzshftral  11777  fz0tp  11788  fzo01  11879  fzo12sn  11880  fzo0to2pr  11881  fzo0to3tp  11882  fzo0to42pr  11883  quoremz  11964  quoremnn0ALT  11966  intfrac2  11967  intfracq  11968  sqval  12209  sqrecii  12232  cu2  12248  i3  12251  i4  12252  binom2i  12259  binom3  12269  crreczi  12273  nn0opthlem1  12330  facp1  12340  faclbnd  12350  faclbnd2  12351  faclbnd4lem1  12353  faclbnd4lem4  12356  bcn1  12373  bcn2  12379  hashgadd  12427  hashxplem  12473  hashmap  12475  hashfun  12477  hashbclem  12483  fz1isolem  12492  ccatlid  12585  ccatrid  12586  eqs1  12603  ccats1val2  12613  ccat2s1p2  12615  ccatw2s1p2  12623  wrdeqs1cat  12682  swrdccatin12lem3  12697  swrdccat3a  12701  cats1fvn  12805  cats1cat  12808  swrds2  12865  reim0  12933  cji  12974  sqrtm1  13091  absi  13101  rddif  13155  iseraltlem2  13487  iseralt  13489  fsump1i  13566  fsummulc2  13581  incexclem  13630  incexc  13631  arisum2  13654  geoihalfsum  13673  mertenslem1  13675  mertens  13677  ef0lem  13796  ege2le3  13807  eft0val  13829  ef4p  13830  efgt1p2  13831  efgt1p  13832  tanval2  13850  efival  13869  ef01bndlem  13901  sin01bnd  13902  cos01bnd  13903  cos1bnd  13904  cos2bnd  13905  rpnnen2lem11  13940  sqr2irrlem  13963  odd2np1lem  14027  odd2np1  14028  oddp1even  14030  divalglem5  14037  divalglem6  14038  bits0  14060  0bits  14071  gcdaddmlem  14148  3prm  14216  phiprm  14289  eulerthlem2  14294  prmdiv  14297  opoe  14317  pythagtriplem12  14332  pythagtriplem14  14334  pcmpt  14393  pcfac  14400  prmpwdvds  14404  pockthi  14407  prmreclem2  14417  prmreclem6  14421  4sqlem5  14442  4sqlem13  14457  modxai  14536  mod2xnegi  14539  gcdi  14541  decexp2  14543  numexpp1  14546  numexp2x  14547  decsplit0b  14548  decsplit1  14550  decsplit  14551  2exp6OLD  14555  2exp16  14557  prmlem0  14573  139prm  14591  163prm  14592  317prm  14593  631prm  14594  1259lem1  14595  1259lem3  14597  1259lem4  14598  1259lem5  14599  1259prm  14600  2503lem1  14601  2503lem2  14602  2503lem3  14603  2503prm  14604  4001lem1  14605  4001lem2  14606  4001lem3  14607  4001lem4  14608  ressinbas  14675  rescfth  15285  xpccatid  15436  oduval  15739  oppgmnd  16368  psgnunilem2  16499  psgnunilem4  16501  psgnpmtr  16514  psgn0fv0  16515  psgnsn  16524  psgnprfval1  16526  lsmmod2  16673  efgi0  16717  efgi1  16718  efginvrel2  16724  efgsval2  16730  efgsp1  16734  efgredleme  16740  efgredlemc  16742  efgcpbllemb  16752  frgpnabllem1  16856  lt6abl  16876  gsumconstf  16934  gsum2dlem2  16977  gsum2dOLD  16979  pwsgsum  16988  pwsgsumOLD  16989  fsfnn0gsumfsffz  16990  dprd0  17057  dprdf1  17059  dprd2da  17070  ablfac1lem  17098  pgpfac1lem3  17107  pgpfaclem1  17111  srgbinomlem4  17173  opprring  17259  mulgass3  17265  evlsval  18167  mpff  18181  ply1assa  18217  gsumply1subr  18254  ply1coe  18316  ply1coeOLD  18317  coe1fzgsumdlem  18322  coe1fzgsumd  18323  gsumply1eq  18326  evl1gsumdlem  18371  evl1gsumd  18372  xrsnsgrp  18433  znbas  18560  znzrh2  18562  dsmmval2  18745  frlmip  18787  matgsum  18917  madetsumid  18941  mdetrsca  19083  mdetrsca2  19084  mdettpos  19091  m2detleiblem2  19108  madugsum  19123  madurid  19124  cpmat  19188  pmatcollpwfi  19261  pmatcollpw3fi1lem1  19265  pm2mpval  19274  mp2pm2mplem5  19289  chpmat1dlem  19314  chpmat1d  19315  chpidmat  19326  cpmidpmat  19352  cpmadugsumfi  19356  chcoeffeqlem  19364  cayleyhamilton0  19368  cayleyhamiltonALT  19370  cayleyhamilton1  19371  restin  19645  imacmp  19875  concompcon  19911  uptx  20104  cnpflf2  20479  tmdgsum2  20573  tsmsresOLD  20623  tsmsres  20624  tsmsf1o  20625  tsmsmhm  20626  prdsxmet  20850  resspwsds  20853  prdsxmslem2  21010  metdcn2  21322  metdcn  21323  metdscn2  21339  iimulcn  21416  icchmeo  21419  xrhmeo  21424  cnrehmeo  21431  cnheiborlem  21432  evth  21437  evth2  21438  lebnumlem2  21440  reparphti  21475  pcoass  21502  pi1xfrcnv  21535  ipcau2  21655  minveclem4  21825  pjthlem1  21830  ovolunlem1a  21885  unmbl  21926  uniioombl  21976  iblitg  22153  dfitg  22154  itg0  22164  iblcnlem1  22172  itgcnlem  22174  itgabs  22219  limcdif  22258  limccnp  22273  limccnp2  22274  dvexp  22334  dvmptid  22338  dvmptc  22339  dvmptfsum  22354  dveflem  22358  dvsincos  22360  mvth  22371  dvlipcn  22373  dvivthlem1  22387  dvfsumle  22400  dvfsumlem2  22406  itgsubst  22428  tdeglem4  22436  tdeglem2  22437  plypf1  22587  plymullem1  22589  coesub  22632  dgrmulc  22646  fta1lem  22681  vieta1lem1  22684  vieta1lem2  22685  aalioulem4  22709  aaliou3lem3  22718  abelthlem2  22805  abelthlem8  22812  abelthlem9  22813  sinhalfpilem  22834  efhalfpi  22842  cospi  22843  efipi  22844  sin2pi  22846  cos2pi  22847  ef2pi  22848  sin2pim  22856  cos2pim  22857  sinmpi  22858  cosmpi  22859  sinppi  22860  cosppi  22861  sincosq4sgn  22872  tangtx  22876  sincos4thpi  22884  sincos6thpi  22886  sincos3rdpi  22887  pige3  22888  abssinper  22889  efif1olem4  22910  efifo  22912  eff1o  22914  circgrp  22917  circsubm  22918  logneg  22950  logimul  22977  logneg2  22978  dvrelog  22996  logcnlem4  23004  dvlog  23010  dvlog2  23012  logtayl  23019  1cxp  23031  ecxp  23032  cxpsqrt  23062  dvsqrt  23096  root1eq1  23107  cxpeq  23109  ang180lem1  23119  ang180lem2  23120  heron  23147  1cubrlem  23150  1cubr  23151  dcubic2  23153  mcubic  23156  cubic2  23157  binom4  23159  dquartlem1  23160  dquartlem2  23161  dquart  23162  quart1lem  23164  quart1  23165  quartlem1  23166  asinsin  23201  asin1  23203  acos1  23204  atanlogsublem  23224  atanlogsub  23225  efiatan2  23226  2efiatan  23227  tanatan  23228  atanbnd  23235  atan1  23237  dvatan  23244  atantayl2  23247  leibpilem2  23250  leibpi  23251  log2cnv  23253  log2tlbnd  23254  log2ublem1  23255  log2ublem2  23256  log2ublem3  23257  log2ub  23258  birthday  23262  amgmlem  23297  emcllem5  23307  wilthlem2  23321  ftalem6  23329  basellem2  23333  basellem3  23334  basellem5  23336  basellem8  23339  cht1  23417  chp1  23419  1sgmprm  23452  ppiublem2  23456  ppiub  23457  chtublem  23464  chtub  23465  logfacbnd3  23476  bcp1ctr  23532  bclbnd  23533  bposlem1  23537  bposlem4  23540  bposlem6  23542  bposlem8  23544  bposlem9  23545  lgslem1  23549  lgsdir2lem1  23576  lgsdir2lem2  23577  lgsdir2lem3  23578  lgsdir2lem5  23580  lgs1  23591  lgseisenlem1  23602  lgseisenlem3  23604  lgsquadlem1  23607  lgsquadlem2  23608  lgsquad2lem2  23612  m1lgs  23615  2sqlem8  23625  2sqblem  23630  logdivsum  23696  mulog2sumlem2  23698  log2sumbnd  23707  selberglem1  23708  selberglem2  23709  pntrmax  23727  pntibndlem2  23754  pntibndlem3  23755  pntlemg  23761  pntlemr  23765  pntlemo  23770  ostth2lem3  23798  ostth2lem4  23799  trgcgrg  23884  colperpexlem1  24082  ax5seglem7  24216  axlowdimlem4  24226  axlowdimlem16  24238  0wlk  24525  0trl  24526  wlkntrllem2  24540  wlkntrl  24542  constr1trl  24568  1pthonlem1  24569  constr2wlk  24578  constr2trl  24579  wlkdvspthlem  24587  constr3trllem3  24630  constr3trllem4  24631  constr3trllem5  24632  constr3pthlem1  24633  constr3pthlem3  24635  clwwlkn2  24753  clwlkisclwwlk2  24768  wwlkext2clwwlk  24781  vdgr1c  24883  nbhashuvtx1  24893  vdegp1ai  24962  vdegp1bi  24963  vdegp1ci  24964  extwwlkfablem2  25056  numclwwlkovf2ex  25064  numclwlk2lem2f  25081  frgraregord013  25096  ex-ind-dvds  25148  smcnlem  25585  ipidsq  25601  dipcj  25605  dip0r  25608  nmlnoubi  25689  nmblolbii  25692  blocnilem  25697  ip1ilem  25719  ip2i  25721  ipdirilem  25722  ipasslem10  25732  ipasslem11  25733  siilem1  25744  hvmul0  25919  hvsubsub4i  25954  hvnegdii  25957  hvsubeq0i  25958  hvsubcan2i  25959  hvsubaddi  25961  hvsub0  25971  hisubcomi  25999  normlem0  26004  normlem1  26005  normlem2  26006  normlem3  26007  normlem9  26013  norm-ii-i  26032  norm3difi  26042  normpari  26049  polid2i  26052  polidi  26053  bcsiALT  26074  pjhthlem1  26287  chdmm3i  26375  chdmm4i  26376  chjidm  26416  chj4i  26419  chjjdiri  26420  spanunsni  26475  pjoml4i  26483  cmcm2i  26489  qlax4i  26526  qlax5i  26527  pjadjii  26570  pjmulii  26573  pjsubii  26574  pjssmii  26577  pjcji  26580  pjneli  26619  hoadd32i  26675  ho0subi  26692  hosubid1  26695  hosd2i  26720  hopncani  26721  hosubeq0i  26723  lnopeq0lem1  26902  lnopunilem1  26907  lnophmlem2  26914  nmbdoplbi  26921  nmcopexi  26924  lnfnmuli  26941  nmcfnexi  26948  nmoptri2i  26996  nmopcoadji  26998  golem1  27168  mdsl1i  27218  cvmdi  27221  mdslmd3i  27229  csmdsymi  27231  xrge00  27652  archirngz  27711  archiabllem2c  27717  gsumle  27748  gsumvsca1  27751  gsumvsca2  27752  xrge0slmod  27812  raddcn  27889  xrge0iifhom  27897  xrge0mulc1cn  27901  cbvesum  28032  gsumesum  28045  esumpfinvallem  28058  esumpfinvalf  28060  dya2icoseg  28226  sitg0  28266  eulerpartlemd  28283  eulerpartlemgvv  28293  eulerpartlemgh  28295  fib0  28316  fib1  28317  fibp1  28318  orrvcval4  28381  orrvcoel  28382  orrvccel  28383  coinflipprob  28396  coinflippvt  28401  ballotlem2  28405  ballotth  28454  signstf0  28503  signstfvn  28504  signsvtn0  28505  signstfvp  28506  signstfveq0  28512  signsvf0  28515  signsvf1  28516  signsvfn  28517  signshf  28523  lgamgulmlem2  28550  lgamgulmlem5  28553  lgam1  28584  subfacp1lem1  28601  subfacp1lem5  28606  subfacval2  28609  subfaclim  28610  subfacval3  28611  cvxpcon  28665  cvxscon  28666  mrsub0  28854  problem4  29000  quad3  29002  sinccvglem  29016  4bc3eq4  29089  4bc2eq6  29090  risefall0lem  29124  risefac1  29131  fallfac1  29132  fallfacfwd  29134  faclimlem1  29144  frrlem5  29367  bpoly0  29788  bpoly1  29789  bpolydiflem  29792  bpoly2  29795  bpoly3  29796  bpoly4  29797  fsumcube  29798  ptrest  30024  dvtan  30041  itgabsnc  30060  ftc1anclem8  30073  dvcnsqrt  30077  dvasin  30079  dvacos  30080  areacirclem1  30083  areacirclem4  30086  areacirc  30088  prdstotbnd  30266  prdsbnd2  30267  repwsmet  30306  rrnequiv  30307  reheibor  30311  mapfzcons  30624  mapfzcons1cl  30626  2rexfrabdioph  30705  3rexfrabdioph  30706  4rexfrabdioph  30707  6rexfrabdioph  30708  7rexfrabdioph  30709  rabdiophlem2  30711  diophren  30723  rabren3dioph  30725  pellexlem5  30745  pell1qr1  30783  rmspecfund  30821  jm2.17a  30874  jm2.17b  30875  jm2.27c  30925  jm2.27dlem5  30931  lmhmlnmsplit  31009  arearect  31159  areaquad  31160  lcmneg  31185  3lcm2e6  31195  lhe4.4ex1a  31210  expgrowthi  31214  expgrowth  31216  refsumcn  31359  oddfl  31413  m1expeven  31539  sumnnodd  31590  cosnegpi  31621  dvcosre  31660  dvsinax  31662  ioodvbdlimc1lem2  31683  ioodvbdlimc2lem  31685  dvmptmulf  31688  dvxpaek  31691  dvmptfprod  31696  dvnprodlem2  31698  dvnprodlem3  31699  itgsin0pilem1  31702  itgsinexplem1  31706  itgsubsticclem  31728  stoweidlem13  31749  wallispilem4  31804  wallispi2lem1  31807  wallispi2lem2  31808  stirlinglem1  31810  dirkerper  31832  dirkertrigeqlem1  31834  dirkertrigeqlem3  31836  dirkertrigeq  31837  dirkeritg  31838  dirkercncflem1  31839  dirkercncflem2  31840  fourierdlem36  31879  fourierdlem41  31884  fourierdlem42  31885  fourierdlem48  31891  fourierdlem56  31899  fourierdlem57  31900  fourierdlem58  31901  fourierdlem60  31903  fourierdlem61  31904  fourierdlem62  31905  fourierdlem65  31908  fourierdlem73  31916  fourierdlem80  31923  fourierdlem87  31930  fourierdlem89  31932  fourierdlem90  31933  fourierdlem91  31934  fourierdlem100  31943  fourierdlem103  31946  fourierdlem107  31950  fourierdlem112  31955  fourierdlem113  31956  fourierdlem115  31958  fouriercnp  31963  sqwvfoura  31965  sqwvfourb  31966  fourierswlem  31967  fouriersw  31968  etransclem2  31973  etransclem37  32008  etransclem46  32017  uhgrepe  32332  2t6m3t4e0  32805  zlmodzxzequa  32967  zlmodzxznm  32968  zlmodzxzequap  32970  sec0  33024  elogb  33039  dalem-cly  35270  pmodN  35449  cdleme0cp  35814  cdleme0cq  35815  cdleme1  35827  cdleme3d  35831  cdleme3h  35835  cdleme4  35838  cdleme5  35840  cdleme7a  35843  cdleme8  35850  cdleme9  35853  cdleme10  35854  cdleme11g  35865  cdleme15b  35875  cdleme21  35938  cdleme22e  35945  cdleme22eALTN  35946  cdleme23c  35952  cdleme25cv  35959  cdleme35b  36051  cdleme35c  36052  cdleme42a  36072  cdleme42d  36074  cdleme43aN  36090  cdlemeg46gfv  36131  cdlemk35  36513  dihjatcclem1  37020  lcdval2  37192  mapdpglem21  37294  inductionexd  37771  unitadd  37820
  Copyright terms: Public domain W3C validator