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

Theorem oveq2i 6207
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 6204 . 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 1399  (class class class)co 6196
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-10 1845  ax-11 1850  ax-12 1862  ax-13 2006  ax-ext 2360
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1402  df-ex 1621  df-nf 1625  df-sb 1748  df-clab 2368  df-cleq 2374  df-clel 2377  df-nfc 2532  df-rex 2738  df-rab 2741  df-v 3036  df-dif 3392  df-un 3394  df-in 3396  df-ss 3403  df-nul 3712  df-if 3858  df-sn 3945  df-pr 3947  df-op 3951  df-uni 4164  df-br 4368  df-iota 5460  df-fv 5504  df-ov 6199
This theorem is referenced by:  caov32  6401  caov4  6405  caov42  6407  seqomsuc  7040  oa1suc  7099  om1  7109  oe1  7111  oawordeulem  7121  oeoalem  7163  nnm1  7215  nnm2  7216  nneob  7219  omopthlem1  7222  mapsnconst  7383  mapsncnv  7384  map2xp  7606  cantnflt  8004  cantnfltOLD  8034  cnfcom2  8059  cnfcom2OLD  8067  infxpenc  8308  infxpenc2  8312  infxpencOLD  8313  infxpenc2OLD  8316  ackbij1lem5  8517  alephom  8873  pwxpndom2  8954  adderpqlem  9243  addassnq  9247  mulcanenq  9249  distrnq  9250  ltanq  9260  ltexnq  9264  halfnq  9265  ltrnq  9268  archnq  9269  addclprlem2  9306  prlem934  9322  prlem936  9336  addcmpblnr  9357  mulcmpblnrlem  9358  ltsrpr  9365  m1p1sr  9380  m1m1sr  9381  0idsr  9385  1idsr  9386  00sr  9387  pn0sr  9389  recexsrlem  9391  mulgt0sr  9393  sqgt0sr  9394  mulresr  9427  axmulcom  9443  axmulass  9445  axdistr  9446  axi2m1  9447  ax1rid  9449  axcnre  9452  mul02lem1  9667  addid1  9671  add42iOLD  9713  negid  9779  negsub  9780  subneg  9781  negsubdii  9818  muleqadd  10110  crne0  10445  2p2e4  10570  3p2e5  10585  3p3e6  10586  4p2e6  10587  4p3e7  10588  4p4e8  10589  5p2e7  10590  5p3e8  10591  5p4e9  10592  5p5e10  10593  6p2e8  10594  6p3e9  10595  6p4e10  10596  7p2e9  10597  7p3e10  10598  8p2e10  10599  3t3e9  10605  8th4div3  10676  halfpm6th  10677  addltmul  10691  nn0n0n1ge2  10776  nneo  10863  zeo  10865  numsuc  10907  numltc  10915  numsucc  10921  numma  10926  nummul1c  10931  6p5lem  10944  4t3lem  10966  decbin2  10999  xmulmnf1  11389  fztp  11658  fzprval  11662  fztpval  11663  fzshftral  11688  fz0tp  11699  fzo01  11796  fzo12sn  11797  fzo0to2pr  11798  fzo0to3tp  11799  fzo0to42pr  11800  quoremz  11882  quoremnn0ALT  11884  intfrac2  11885  intfracq  11886  sqval  12130  sqrecii  12153  cu2  12169  i3  12172  i4  12173  binom2i  12180  binom3  12189  crreczi  12193  nn0opthlem1  12250  facp1  12260  faclbnd  12270  faclbnd2  12271  faclbnd4lem1  12273  faclbnd4lem4  12276  bcn1  12293  bcn2  12299  hashgadd  12348  hashxplem  12395  hashmap  12397  hashfun  12399  hashbclem  12405  fz1isolem  12414  ccatlid  12512  ccatrid  12513  ccats1val2  12540  ccat2s1p2  12542  wrdeqs1cat  12611  swrdccatin12lem3  12626  swrdccat3a  12630  cats1fvn  12734  cats1cat  12737  swrds2  12794  reim0  12953  cji  12994  sqrtm1  13111  absi  13121  rddif  13175  iseraltlem2  13507  iseralt  13509  fsump1i  13586  fsummulc2  13601  incexclem  13650  incexc  13651  arisum2  13674  geoihalfsum  13693  mertenslem1  13695  mertens  13697  ef0lem  13816  ege2le3  13827  eft0val  13849  ef4p  13850  efgt1p2  13851  efgt1p  13852  tanval2  13870  efival  13889  ef01bndlem  13921  sin01bnd  13922  cos01bnd  13923  cos1bnd  13924  cos2bnd  13925  rpnnen2lem11  13960  sqr2irrlem  13983  odd2np1lem  14047  odd2np1  14048  oddp1even  14050  divalglem5  14057  divalglem6  14058  bits0  14080  0bits  14091  gcdaddmlem  14168  3prm  14236  phiprm  14309  eulerthlem2  14314  prmdiv  14317  opoe  14337  pythagtriplem12  14352  pythagtriplem14  14354  pcmpt  14413  pcfac  14420  prmpwdvds  14424  pockthi  14427  prmreclem2  14437  prmreclem6  14441  4sqlem5  14462  4sqlem13  14477  modxai  14556  mod2xnegi  14559  gcdi  14561  decexp2  14563  numexpp1  14566  numexp2x  14567  decsplit0b  14568  decsplit1  14570  decsplit  14571  2exp6OLD  14575  2exp16  14577  prmlem0  14593  139prm  14611  163prm  14612  317prm  14613  631prm  14614  1259lem1  14615  1259lem3  14617  1259lem4  14618  1259lem5  14619  1259prm  14620  2503lem1  14621  2503lem2  14622  2503lem3  14623  2503prm  14624  4001lem1  14625  4001lem2  14626  4001lem3  14627  4001lem4  14628  ressinbas  14697  rcaninv  15200  rescfth  15343  xpccatid  15574  oduval  15877  oppgmnd  16506  psgnunilem2  16637  psgnunilem4  16639  psgnpmtr  16652  psgn0fv0  16653  psgnsn  16662  psgnprfval1  16664  lsmmod2  16811  efgi0  16855  efgi1  16856  efginvrel2  16862  efgsval2  16868  efgsp1  16872  efgredleme  16878  efgredlemc  16880  efgcpbllemb  16890  frgpnabllem1  16994  lt6abl  17014  gsumconstf  17071  gsum2dlem2  17112  gsum2dOLD  17114  pwsgsum  17122  pwsgsumOLD  17123  fsfnn0gsumfsffz  17124  dprd0  17191  dprdf1  17193  dprd2da  17204  ablfac1lem  17232  pgpfac1lem3  17241  pgpfaclem1  17245  srgbinomlem4  17307  opprring  17393  mulgass3  17399  evlsval  18301  mpff  18315  ply1assa  18351  gsumply1subr  18388  ply1coe  18450  ply1coeOLD  18451  coe1fzgsumdlem  18456  coe1fzgsumd  18457  gsumply1eq  18460  evl1gsumdlem  18505  evl1gsumd  18506  xrsnsgrp  18567  znbas  18673  znzrh2  18675  dsmmval2  18858  frlmip  18898  matgsum  19024  madetsumid  19048  mdetrsca  19190  mdetrsca2  19191  mdettpos  19198  m2detleiblem2  19215  madugsum  19230  madurid  19231  cpmat  19295  pmatcollpwfi  19368  pmatcollpw3fi1lem1  19372  pm2mpval  19381  mp2pm2mplem5  19396  chpmat1dlem  19421  chpmat1d  19422  chpidmat  19433  cpmidpmat  19459  cpmadugsumfi  19463  chcoeffeqlem  19471  cayleyhamilton0  19475  cayleyhamiltonALT  19477  cayleyhamilton1  19478  restin  19753  imacmp  19983  concompcon  20018  uptx  20211  cnpflf2  20586  tmdgsum2  20680  tsmsresOLD  20730  tsmsres  20731  tsmsf1o  20732  tsmsmhm  20733  prdsxmet  20957  resspwsds  20960  prdsxmslem2  21117  metdcn2  21429  metdcn  21430  metdscn2  21446  iimulcn  21523  icchmeo  21526  xrhmeo  21531  cnrehmeo  21538  cnheiborlem  21539  evth  21544  evth2  21545  lebnumlem2  21547  reparphti  21582  pcoass  21609  pi1xfrcnv  21642  ipcau2  21762  minveclem4  21932  pjthlem1  21937  ovolunlem1a  21992  unmbl  22033  uniioombl  22083  iblitg  22260  dfitg  22261  itg0  22271  iblcnlem1  22279  itgcnlem  22281  itgabs  22326  limcdif  22365  limccnp  22380  limccnp2  22381  dvexp  22441  dvmptid  22445  dvmptc  22446  dvmptfsum  22461  dveflem  22465  dvsincos  22467  mvth  22478  dvlipcn  22480  dvivthlem1  22494  dvfsumle  22507  dvfsumlem2  22513  itgsubst  22535  tdeglem4  22543  tdeglem2  22544  plypf1  22694  plymullem1  22696  coesub  22739  dgrmulc  22753  fta1lem  22788  vieta1lem1  22791  vieta1lem2  22792  aalioulem4  22816  aaliou3lem3  22825  abelthlem2  22912  abelthlem8  22919  abelthlem9  22920  sinhalfpilem  22941  efhalfpi  22949  cospi  22950  efipi  22951  sin2pi  22953  cos2pi  22954  ef2pi  22955  sin2pim  22963  cos2pim  22964  sinmpi  22965  cosmpi  22966  sinppi  22967  cosppi  22968  sincosq4sgn  22979  tangtx  22983  sincos4thpi  22991  sincos6thpi  22993  sincos3rdpi  22994  pige3  22995  abssinper  22996  efif1olem4  23017  efifo  23019  eff1o  23021  circgrp  23024  circsubm  23025  logneg  23060  logimul  23086  logneg2  23087  dvrelog  23105  logcnlem4  23113  dvlog  23119  dvlog2  23121  logtayl  23128  1cxp  23140  ecxp  23141  cxpsqrt  23171  dvsqrt  23205  root1eq1  23216  cxpeq  23218  elogb  23228  ang180lem1  23259  ang180lem2  23260  heron  23285  1cubrlem  23288  1cubr  23289  dcubic2  23291  mcubic  23294  cubic2  23295  binom4  23297  dquartlem1  23298  dquartlem2  23299  dquart  23300  quart1lem  23302  quart1  23303  quartlem1  23304  asinsin  23339  asin1  23341  acos1  23342  atanlogsublem  23362  atanlogsub  23363  efiatan2  23364  2efiatan  23365  tanatan  23366  atanbnd  23373  atan1  23375  dvatan  23382  atantayl2  23385  leibpilem2  23388  leibpi  23389  log2cnv  23391  log2tlbnd  23392  log2ublem1  23393  log2ublem2  23394  log2ublem3  23395  log2ub  23396  birthday  23401  amgmlem  23436  emcllem5  23446  wilthlem2  23460  ftalem6  23468  basellem2  23472  basellem3  23473  basellem5  23475  basellem8  23478  cht1  23556  chp1  23558  1sgmprm  23591  ppiublem2  23595  ppiub  23596  chtublem  23603  chtub  23604  logfacbnd3  23615  bcp1ctr  23671  bclbnd  23672  bposlem1  23676  bposlem4  23679  bposlem6  23681  bposlem8  23683  bposlem9  23684  lgslem1  23688  lgsdir2lem1  23715  lgsdir2lem2  23716  lgsdir2lem3  23717  lgsdir2lem5  23719  lgs1  23730  lgseisenlem1  23741  lgseisenlem3  23743  lgsquadlem1  23746  lgsquadlem2  23747  lgsquad2lem2  23751  m1lgs  23754  2sqlem8  23764  2sqblem  23769  logdivsum  23835  mulog2sumlem2  23837  log2sumbnd  23846  selberglem1  23847  selberglem2  23848  pntrmax  23866  pntibndlem2  23893  pntibndlem3  23894  pntlemg  23900  pntlemr  23904  pntlemo  23909  ostth2lem3  23937  ostth2lem4  23938  trgcgrg  24026  colperpexlem1  24224  ax5seglem7  24359  axlowdimlem4  24369  axlowdimlem16  24381  0wlk  24668  0trl  24669  wlkntrllem2  24683  wlkntrl  24685  constr1trl  24711  1pthonlem1  24712  constr2wlk  24721  constr2trl  24722  wlkdvspthlem  24730  constr3trllem3  24773  constr3trllem4  24774  constr3trllem5  24775  constr3pthlem1  24776  constr3pthlem3  24778  clwwlkn2  24896  clwlkisclwwlk2  24911  wwlkext2clwwlk  24924  vdgr1c  25026  nbhashuvtx1  25036  vdegp1ai  25105  vdegp1bi  25106  vdegp1ci  25107  extwwlkfablem2  25199  numclwwlkovf2ex  25207  numclwlk2lem2f  25224  frgraregord013  25239  ex-ind-dvds  25291  smcnlem  25724  ipidsq  25740  dipcj  25744  dip0r  25747  nmlnoubi  25828  nmblolbii  25831  blocnilem  25836  ip1ilem  25858  ip2i  25860  ipdirilem  25861  ipasslem10  25871  ipasslem11  25872  siilem1  25883  hvmul0  26058  hvsubsub4i  26093  hvnegdii  26096  hvsubeq0i  26097  hvsubcan2i  26098  hvsubaddi  26100  hvsub0  26110  hisubcomi  26138  normlem0  26143  normlem1  26144  normlem2  26145  normlem3  26146  normlem9  26152  norm-ii-i  26171  norm3difi  26181  normpari  26188  polid2i  26191  polidi  26192  bcsiALT  26213  pjhthlem1  26426  chdmm3i  26514  chdmm4i  26515  chjidm  26555  chj4i  26558  chjjdiri  26559  spanunsni  26614  pjoml4i  26622  cmcm2i  26628  qlax4i  26665  qlax5i  26666  pjadjii  26709  pjmulii  26712  pjsubii  26713  pjssmii  26716  pjcji  26719  pjneli  26758  hoadd32i  26813  ho0subi  26830  hosubid1  26833  hosd2i  26858  hopncani  26859  hosubeq0i  26861  lnopeq0lem1  27040  lnopunilem1  27045  lnophmlem2  27052  nmbdoplbi  27059  nmcopexi  27062  lnfnmuli  27079  nmcfnexi  27086  nmoptri2i  27134  nmopcoadji  27136  golem1  27306  mdsl1i  27356  cvmdi  27359  mdslmd3i  27367  csmdsymi  27369  xrge00  27827  archirngz  27886  archiabllem2c  27892  gsumle  27923  gsummpt2co  27924  gsumvsca1  27927  gsumvsca2  27928  xrge0slmod  27988  raddcn  28065  xrge0iifhom  28073  xrge0mulc1cn  28077  cbvesum  28190  gsumesum  28207  esumpfinvallem  28222  esumpfinvalf  28224  dya2icoseg  28404  sitg0  28471  eulerpartlemd  28488  eulerpartlemgvv  28498  eulerpartlemgh  28500  fib0  28521  fib1  28522  fibp1  28523  orrvcval4  28586  orrvcoel  28587  orrvccel  28588  coinflipprob  28601  coinflippvt  28606  ballotlem2  28610  ballotth  28659  signstf0  28708  signstfvn  28709  signsvtn0  28710  signstfvp  28711  signstfveq0  28717  signsvf0  28720  signsvf1  28721  signsvfn  28722  signshf  28728  lgamgulmlem2  28761  lgamgulmlem5  28764  lgam1  28795  subfacp1lem1  28812  subfacp1lem5  28817  subfacval2  28820  subfaclim  28821  subfacval3  28822  cvxpcon  28876  cvxscon  28877  mrsub0  29065  problem4  29211  quad3  29213  sinccvglem  29227  4bc3eq4  29277  4bc2eq6  29278  iexpire  29288  risefall0lem  29314  risefac1  29321  fallfac1  29322  fallfacfwd  29324  faclimlem1  29334  frrlem5  29556  bpoly0  29965  bpoly1  29966  bpolydiflem  29969  bpoly2  29972  bpoly3  29973  bpoly4  29974  fsumcube  29975  ptrest  30213  dvtan  30231  itgabsnc  30250  ftc1anclem8  30263  dvcnsqrt  30267  dvasin  30269  dvacos  30270  areacirclem1  30273  areacirclem4  30276  areacirc  30278  prdstotbnd  30456  prdsbnd2  30457  repwsmet  30496  rrnequiv  30497  reheibor  30501  mapfzcons  30814  mapfzcons1cl  30816  2rexfrabdioph  30895  3rexfrabdioph  30896  4rexfrabdioph  30897  6rexfrabdioph  30898  7rexfrabdioph  30899  rabdiophlem2  30901  diophren  30912  rabren3dioph  30914  pellexlem5  30934  pell1qr1  30972  rmspecfund  31010  jm2.17a  31063  jm2.17b  31064  jm2.27c  31115  jm2.27dlem5  31121  lmhmlnmsplit  31199  arearect  31351  areaquad  31352  lcmneg  31377  3lcm2e6  31387  lhe4.4ex1a  31402  expgrowthi  31406  expgrowth  31408  bccn1  31417  binomcxplemdvbinom  31426  binomcxplemdvsum  31428  binomcxplemnotnn0  31429  binomcxp  31430  refsumcn  31572  oddfl  31626  m1expeven  31751  sumnnodd  31802  cosnegpi  31833  dvcosre  31872  dvsinax  31874  ioodvbdlimc1lem2  31895  ioodvbdlimc2lem  31897  dvmptmulf  31900  dvxpaek  31903  dvmptfprod  31908  dvnprodlem2  31910  dvnprodlem3  31911  itgsin0pilem1  31914  itgsinexplem1  31918  itgsubsticclem  31940  stoweidlem13  31961  wallispilem4  32016  wallispi2lem1  32019  wallispi2lem2  32020  stirlinglem1  32022  dirkerper  32044  dirkertrigeqlem1  32046  dirkertrigeqlem3  32048  dirkertrigeq  32049  dirkeritg  32050  dirkercncflem1  32051  dirkercncflem2  32052  fourierdlem36  32091  fourierdlem41  32096  fourierdlem42  32097  fourierdlem48  32103  fourierdlem56  32111  fourierdlem57  32112  fourierdlem58  32113  fourierdlem60  32115  fourierdlem61  32116  fourierdlem62  32117  fourierdlem65  32120  fourierdlem73  32128  fourierdlem80  32135  fourierdlem87  32142  fourierdlem89  32144  fourierdlem90  32145  fourierdlem91  32146  fourierdlem100  32155  fourierdlem103  32158  fourierdlem107  32162  fourierdlem112  32167  fourierdlem113  32168  fourierdlem115  32170  fouriercnp  32175  sqwvfoura  32177  sqwvfourb  32178  fourierswlem  32179  fouriersw  32180  etransclem2  32185  etransclem37  32220  etransclem46  32229  bits0ALTV  32521  5tcu2e40  32549  3exp4mod41  32550  41prothprmlem1  32551  41prothprmlem2  32552  41prothprm  32553  pfx1  32586  pfxccatpfx1  32602  pfxccatpfx2  32603  uhgrepe  32696  2t6m3t4e0  33137  zlmodzxzequa  33297  zlmodzxznm  33298  zlmodzxzequap  33300  nn0sumshdiglemA  33440  nn0sumshdiglemB  33441  nn0sumshdiglem1  33442  sec0  33490  dalem-cly  35808  pmodN  35987  cdleme0cp  36352  cdleme0cq  36353  cdleme1  36365  cdleme3d  36369  cdleme3h  36373  cdleme4  36376  cdleme5  36378  cdleme7a  36381  cdleme8  36388  cdleme9  36391  cdleme10  36392  cdleme11g  36403  cdleme15b  36413  cdleme21  36476  cdleme22e  36483  cdleme22eALTN  36484  cdleme23c  36490  cdleme25cv  36497  cdleme35b  36589  cdleme35c  36590  cdleme42a  36610  cdleme42d  36612  cdleme43aN  36628  cdlemeg46gfv  36669  cdlemk35  37051  dihjatcclem1  37558  lcdval2  37730  mapdpglem21  37832  relexp2  38216  inductionexd  38496  unitadd  38545
  Copyright terms: Public domain W3C validator