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

Theorem oveq2i 6293
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 6290 . 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 1379  (class class class)co 6282
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-rex 2820  df-rab 2823  df-v 3115  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-nul 3786  df-if 3940  df-sn 4028  df-pr 4030  df-op 4034  df-uni 4246  df-br 4448  df-iota 5549  df-fv 5594  df-ov 6285
This theorem is referenced by:  caov32  6484  caov4  6488  caov42  6490  seqomsuc  7119  oa1suc  7178  om1  7188  oe1  7190  oawordeulem  7200  oeoalem  7242  nnm1  7294  nnm2  7295  nneob  7298  omopthlem1  7301  mapsnconst  7461  mapsncnv  7462  map2xp  7684  cantnflt  8087  cantnfltOLD  8117  cnfcom2  8142  cnfcom2OLD  8150  infxpenc  8391  infxpenc2  8395  infxpencOLD  8396  infxpenc2OLD  8399  ackbij1lem5  8600  alephom  8956  pwxpndom2  9039  adderpqlem  9328  addassnq  9332  mulcanenq  9334  distrnq  9335  ltanq  9345  ltexnq  9349  halfnq  9350  ltrnq  9353  archnq  9354  addclprlem2  9391  prlem934  9407  prlem936  9421  addcmpblnr  9442  mulcmpblnrlem  9443  ltsrpr  9450  m1p1sr  9465  m1m1sr  9466  0idsr  9470  1idsr  9471  00sr  9472  pn0sr  9474  recexsrlem  9476  mulgt0sr  9478  sqgt0sr  9479  mulresr  9512  axmulcom  9528  axmulass  9530  axdistr  9531  axi2m1  9532  ax1rid  9534  axcnre  9537  mul02lem1  9751  addid1  9755  add42i  9796  negid  9862  negsub  9863  subneg  9864  negsubdii  9900  muleqadd  10189  crne0  10525  2p2e4  10649  3p2e5  10664  3p3e6  10665  4p2e6  10666  4p3e7  10667  4p4e8  10668  5p2e7  10669  5p3e8  10670  5p4e9  10671  5p5e10  10672  6p2e8  10673  6p3e9  10674  6p4e10  10675  7p2e9  10676  7p3e10  10677  8p2e10  10678  3t3e9  10684  8th4div3  10755  halfpm6th  10756  addltmul  10770  nn0n0n1ge2  10855  nneo  10940  zeo  10942  numsuc  10984  numltc  10992  numsucc  10998  numma  11003  nummul1c  11008  6p5lem  11021  4t3lem  11043  decbin2  11076  xmulmnf1  11464  fztp  11732  fzprval  11736  fztpval  11737  fzshftral  11761  fz0tp  11771  fzo01  11861  fzo12sn  11862  fzo0to2pr  11863  fzo0to3tp  11864  fzo0to42pr  11865  quoremz  11945  quoremnn0ALT  11947  intfrac2  11948  intfracq  11949  f13idfv  12069  sqval  12189  sqrecii  12212  cu2  12228  i3  12231  i4  12232  binom2i  12239  binom3  12249  crreczi  12253  nn0opthlem1  12310  facp1  12320  faclbnd  12330  faclbnd2  12331  faclbnd4lem1  12333  faclbnd4lem4  12336  bcn1  12353  bcn2  12359  hashgadd  12407  hashxplem  12451  hashmap  12453  hashfun  12455  hashbclem  12461  fz1isolem  12470  ccatlid  12562  ccatrid  12563  eqs1  12578  ccats1val2  12588  ccat2s1p2  12590  ccatw2s1p2  12598  wrdeqs1cat  12657  cats1un  12658  swrdccatin12lem3  12672  swrdccat3a  12676  cats1fvn  12780  cats1cat  12783  swrds2  12840  reim0  12908  cji  12949  sqrtm1  13066  absi  13076  rddif  13129  iseraltlem2  13461  iseralt  13463  fsump1i  13540  fsummulc2  13555  incexclem  13604  incexc  13605  arisum2  13628  geoihalfsum  13647  mertenslem1  13649  mertens  13651  ef0lem  13669  ege2le3  13680  eft0val  13701  ef4p  13702  efgt1p2  13703  efgt1p  13704  tanval2  13722  efival  13741  ef01bndlem  13773  sin01bnd  13774  cos01bnd  13775  cos1bnd  13776  cos2bnd  13777  rpnnen2lem11  13812  sqr2irrlem  13835  odd2np1lem  13897  odd2np1  13898  oddp1even  13900  divalglem5  13907  divalglem6  13908  bits0  13930  0bits  13941  gcdaddmlem  14018  3prm  14086  phiprm  14159  eulerthlem2  14164  prmdiv  14167  opoe  14187  pythagtriplem12  14202  pythagtriplem14  14204  pcmpt  14263  pcfac  14270  prmpwdvds  14274  pockthi  14277  prmreclem2  14287  prmreclem6  14291  4sqlem5  14312  4sqlem13  14327  modxai  14406  mod2xnegi  14409  gcdi  14411  decexp2  14413  numexpp1  14416  numexp2x  14417  decsplit0b  14418  decsplit1  14420  decsplit  14421  2exp6  14424  2exp16  14426  prmlem0  14442  139prm  14460  163prm  14461  317prm  14462  631prm  14463  1259lem1  14464  1259lem3  14466  1259lem4  14467  1259lem5  14468  1259prm  14469  2503lem1  14470  2503lem2  14471  2503lem3  14472  2503prm  14473  4001lem1  14474  4001lem2  14475  4001lem3  14476  4001lem4  14477  ressinbas  14544  rescfth  15157  xpccatid  15308  oduval  15610  oppgmnd  16181  psgnunilem2  16313  psgnunilem4  16315  psgnpmtr  16328  psgn0fv0  16329  psgnsn  16338  psgnprfval1  16340  lsmmod2  16487  efgi0  16531  efgi1  16532  efginvrel2  16538  efgsval2  16544  efgsp1  16548  efgredleme  16554  efgredlemc  16556  efgcpbllemb  16566  frgpnabllem1  16665  lt6abl  16685  gsumconstf  16743  gsum2dlem2  16786  gsum2dOLD  16788  pwsgsum  16797  pwsgsumOLD  16798  fsfnn0gsumfsffz  16799  dprd0  16865  dprdf1  16867  dprd2da  16878  ablfac1lem  16906  pgpfac1lem3  16915  pgpfaclem1  16919  srgbinomlem4  16979  opprrng  17061  mulgass3  17067  evlsval  17956  mpff  17970  ply1assa  18006  gsumply1subr  18043  ply1coe  18105  ply1coeOLD  18106  coe1fzgsumdlem  18111  coe1fzgsumd  18112  gsumply1eq  18115  evl1gsumdlem  18160  evl1gsumd  18161  znbas  18346  znzrh2  18348  dsmmval2  18531  frlmip  18573  matgsum  18703  madetsumid  18727  mdetrsca  18869  mdetrsca2  18870  mdettpos  18877  m2detleiblem2  18894  madugsum  18909  madurid  18910  cpmat  18974  pmatcollpwfi  19047  pmatcollpw3fi1lem1  19051  pm2mpval  19060  mp2pm2mplem5  19075  chpmat1dlem  19100  chpmat1d  19101  chpidmat  19112  cpmidpmat  19138  cpmadugsumfi  19142  chcoeffeqlem  19150  cayleyhamilton0  19154  cayleyhamiltonALT  19156  cayleyhamilton1  19157  restin  19430  imacmp  19660  concompcon  19696  uptx  19858  cnpflf2  20233  tmdgsum2  20327  tsmsresOLD  20377  tsmsres  20378  tsmsf1o  20379  tsmsmhm  20380  prdsxmet  20604  resspwsds  20607  prdsxmslem2  20764  metdcn2  21076  metdcn  21077  metdscn2  21093  iimulcn  21170  icchmeo  21173  xrhmeo  21178  cnrehmeo  21185  cnheiborlem  21186  evth  21191  evth2  21192  lebnumlem2  21194  reparphti  21229  pcoass  21256  pi1xfrcnv  21289  ipcau2  21409  minveclem4  21579  pjthlem1  21584  ovolunlem1a  21639  unmbl  21680  uniioombl  21730  iblitg  21907  dfitg  21908  itg0  21918  iblcnlem1  21926  itgcnlem  21928  itgabs  21973  limcdif  22012  limccnp  22027  limccnp2  22028  dvexp  22088  dvmptid  22092  dvmptc  22093  dvmptfsum  22108  dveflem  22112  dvsincos  22114  mvth  22125  dvlipcn  22127  dvivthlem1  22141  dvfsumle  22154  dvfsumlem2  22160  itgsubst  22182  tdeglem4  22190  tdeglem2  22191  plypf1  22341  plymullem1  22343  coesub  22385  dgrmulc  22399  fta1lem  22434  vieta1lem1  22437  vieta1lem2  22438  aalioulem4  22462  aaliou3lem3  22471  abelthlem2  22558  abelthlem8  22565  abelthlem9  22566  sinhalfpilem  22586  efhalfpi  22594  cospi  22595  efipi  22596  sin2pi  22598  cos2pi  22599  ef2pi  22600  sin2pim  22608  cos2pim  22609  sinmpi  22610  cosmpi  22611  sinppi  22612  cosppi  22613  sincosq4sgn  22624  tangtx  22628  sincos4thpi  22636  sincos6thpi  22638  sincos3rdpi  22639  pige3  22640  abssinper  22641  efif1olem4  22662  efifo  22664  eff1o  22666  logneg  22697  logimul  22724  logneg2  22725  dvrelog  22743  logcnlem4  22751  dvlog  22757  dvlog2  22759  logtayl  22766  1cxp  22778  ecxp  22779  cxpsqrt  22809  dvsqrt  22843  root1eq1  22854  cxpeq  22856  ang180lem1  22866  ang180lem2  22867  heron  22894  1cubrlem  22897  1cubr  22898  dcubic2  22900  mcubic  22903  cubic2  22904  binom4  22906  dquartlem1  22907  dquartlem2  22908  dquart  22909  quart1lem  22911  quart1  22912  quartlem1  22913  asinsin  22948  asin1  22950  acos1  22951  atanlogsublem  22971  atanlogsub  22972  efiatan2  22973  2efiatan  22974  tanatan  22975  atanbnd  22982  atan1  22984  dvatan  22991  atantayl2  22994  leibpilem2  22997  leibpi  22998  log2cnv  23000  log2tlbnd  23001  log2ublem1  23002  log2ublem2  23003  log2ublem3  23004  log2ub  23005  birthday  23009  amgmlem  23044  emcllem5  23054  wilthlem2  23068  ftalem6  23076  basellem2  23080  basellem3  23081  basellem5  23083  basellem8  23086  cht1  23164  chp1  23166  1sgmprm  23199  ppiublem2  23203  ppiub  23204  chtublem  23211  chtub  23212  logfacbnd3  23223  bcp1ctr  23279  bclbnd  23280  bposlem1  23284  bposlem4  23287  bposlem6  23289  bposlem8  23291  bposlem9  23292  lgslem1  23296  lgsdir2lem1  23323  lgsdir2lem2  23324  lgsdir2lem3  23325  lgsdir2lem5  23327  lgs1  23338  lgseisenlem1  23349  lgseisenlem3  23351  lgsquadlem1  23354  lgsquadlem2  23355  lgsquad2lem2  23359  m1lgs  23362  2sqlem8  23372  2sqblem  23377  logdivsum  23443  mulog2sumlem2  23445  log2sumbnd  23454  selberglem1  23455  selberglem2  23456  pntrmax  23474  pntibndlem2  23501  pntibndlem3  23502  pntlemg  23508  pntlemr  23512  pntlemo  23517  ostth2lem3  23545  ostth2lem4  23546  trgcgrg  23631  colperpexlem1  23806  ax5seglem7  23911  axlowdimlem4  23921  axlowdimlem16  23933  0wlk  24220  0trl  24221  wlkntrllem2  24235  wlkntrl  24237  constr1trl  24263  1pthonlem1  24264  constr2wlk  24273  constr2trl  24274  wlkdvspthlem  24282  constr3trllem3  24325  constr3trllem4  24326  constr3trllem5  24327  constr3pthlem1  24328  constr3pthlem3  24330  clwwlkn2  24448  clwlkisclwwlk2  24463  wwlkext2clwwlk  24476  vdgr1c  24578  nbhashuvtx1  24588  vdegp1ai  24657  vdegp1bi  24658  vdegp1ci  24659  extwwlkfablem2  24752  numclwwlkovf2ex  24760  numclwlk2lem2f  24777  frgraregord013  24792  smcnlem  25280  ipidsq  25296  dipcj  25300  dip0r  25303  nmlnoubi  25384  nmblolbii  25387  blocnilem  25392  ip1ilem  25414  ip2i  25416  ipdirilem  25417  ipasslem10  25427  ipasslem11  25428  siilem1  25439  hvmul0  25614  hvsubsub4i  25649  hvnegdii  25652  hvsubeq0i  25653  hvsubcan2i  25654  hvsubaddi  25656  hvsub0  25666  hisubcomi  25694  normlem0  25699  normlem1  25700  normlem2  25701  normlem3  25702  normlem9  25708  norm-ii-i  25727  norm3difi  25737  normpari  25744  polid2i  25747  polidi  25748  bcsiALT  25769  pjhthlem1  25982  chdmm3i  26070  chdmm4i  26071  chjidm  26111  chj4i  26114  chjjdiri  26115  spanunsni  26170  pjoml4i  26178  cmcm2i  26184  qlax4i  26221  qlax5i  26222  pjadjii  26265  pjmulii  26268  pjsubii  26269  pjssmii  26272  pjcji  26275  pjneli  26314  hoadd32i  26370  ho0subi  26387  hosubid1  26390  hosd2i  26415  hopncani  26416  hosubeq0i  26418  lnopeq0lem1  26597  lnopunilem1  26602  lnophmlem2  26609  nmbdoplbi  26616  nmcopexi  26619  lnfnmuli  26636  nmcfnexi  26643  nmoptri2i  26691  nmopcoadji  26693  golem1  26863  mdsl1i  26913  cvmdi  26916  mdslmd3i  26924  csmdsymi  26926  xrge00  27333  archirngz  27392  archiabllem2c  27398  gsumle  27430  gsumvsca1  27433  gsumvsca2  27434  xrge0slmod  27494  raddcn  27544  xrge0iifhom  27552  xrge0mulc1cn  27556  cbvesum  27691  gsumesum  27704  esumpfinvallem  27717  esumpfinvalf  27719  dya2icoseg  27885  sitg0  27925  eulerpartlemd  27942  eulerpartlemgvv  27952  eulerpartlemgh  27954  fib0  27975  fib1  27976  fibp1  27977  orrvcval4  28040  orrvcoel  28041  orrvccel  28042  coinflipprob  28055  coinflippvt  28060  ballotlem2  28064  ballotth  28113  signstf0  28162  signstfvn  28163  signsvtn0  28164  signstfvp  28165  signstfvneq0  28166  signstfveq0  28171  signsvf0  28174  signsvf1  28175  signsvfn  28176  signshf  28182  lgamgulmlem2  28209  lgamgulmlem5  28212  lgam1  28243  subfacp1lem1  28260  subfacp1lem5  28265  subfacval2  28268  subfaclim  28269  subfacval3  28270  cvxpcon  28324  cvxscon  28325  problem4  28494  quad3  28496  sinccvglem  28510  4bc3eq4  28583  4bc2eq6  28584  risefall0lem  28722  risefac1  28729  fallfac1  28730  fallfacfwd  28732  faclimlem1  28742  frrlem5  28965  bpoly0  29386  bpoly1  29387  bpolydiflem  29390  bpoly2  29393  bpoly3  29394  bpoly4  29395  fsumcube  29396  ptrest  29623  dvtan  29640  itgabsnc  29659  ftc1anclem8  29672  dvcnsqrt  29676  dvasin  29678  dvacos  29679  areacirclem1  29682  areacirclem4  29685  areacirc  29687  prdstotbnd  29891  prdsbnd2  29892  repwsmet  29931  rrnequiv  29932  reheibor  29936  mapfzcons  30250  mapfzcons1cl  30252  2rexfrabdioph  30331  3rexfrabdioph  30332  4rexfrabdioph  30333  6rexfrabdioph  30334  7rexfrabdioph  30335  rabdiophlem2  30337  diophren  30349  rabren3dioph  30351  pellexlem5  30371  pell1qr1  30409  rmspecfund  30447  jm2.17a  30500  jm2.17b  30501  jm2.27c  30553  jm2.27dlem5  30559  lmhmlnmsplit  30637  arearect  30788  areaquad  30789  lcmneg  30809  3lcm2e6  30819  lhe4.4ex1a  30834  expgrowthi  30838  expgrowth  30840  refsumcn  30983  oddfl  31036  m1expeven  31141  sumnnodd  31172  cosnegpi  31203  icocncflimc  31228  dvcosre  31239  dvsinax  31241  ioodvbdlimc1lem2  31262  ioodvbdlimc2lem  31264  itgsin0pilem1  31267  itgsinexplem1  31271  itgsubsticclem  31293  stoweidlem13  31313  wallispilem4  31368  wallispi2lem1  31371  wallispi2lem2  31372  stirlinglem1  31374  dirkerper  31396  dirkertrigeqlem1  31398  dirkertrigeqlem3  31400  dirkertrigeq  31401  dirkeritg  31402  dirkercncflem1  31403  dirkercncflem2  31404  fourierdlem36  31443  fourierdlem41  31448  fourierdlem42  31449  fourierdlem48  31455  fourierdlem56  31463  fourierdlem57  31464  fourierdlem58  31465  fourierdlem60  31467  fourierdlem61  31468  fourierdlem62  31469  fourierdlem65  31472  fourierdlem73  31480  fourierdlem80  31487  fourierdlem87  31494  fourierdlem89  31496  fourierdlem90  31497  fourierdlem91  31498  fourierdlem100  31507  fourierdlem103  31510  fourierdlem107  31514  fourierdlem112  31519  fourierdlem113  31520  fourierdlem115  31522  fouriercnp  31527  sqwvfoura  31529  sqwvfourb  31530  fourierswlem  31531  fouriersw  31532  uhgrepe  31847  2t6m3t4e0  32001  zlmodzxzequa  32178  zlmodzxznm  32179  zlmodzxzequap  32181  sec0  32235  elogb  32250  dalem-cly  34467  pmodN  34646  cdleme0cp  35010  cdleme0cq  35011  cdleme1  35023  cdleme3d  35027  cdleme3h  35031  cdleme4  35034  cdleme5  35036  cdleme7a  35039  cdleme8  35046  cdleme9  35049  cdleme10  35050  cdleme11g  35061  cdleme15b  35071  cdleme21  35133  cdleme22e  35140  cdleme22eALTN  35141  cdleme23c  35147  cdleme25cv  35154  cdleme35b  35246  cdleme35c  35247  cdleme42a  35267  cdleme42d  35269  cdleme43aN  35285  cdlemeg46gfv  35326  cdlemk35  35708  dihjatcclem1  36215  lcdval2  36387  mapdpglem21  36489
  Copyright terms: Public domain W3C validator