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

Theorem oveq2i 5871
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 5868 . 2  |-  ( A  =  B  ->  ( C F A )  =  ( C F B ) )
31, 2ax-mp 8 1  |-  ( C F A )  =  ( C F B )
Colors of variables: wff set class
Syntax hints:    = wceq 1625  (class class class)co 5860
This theorem is referenced by:  caov32  6049  caov4  6053  caov42  6055  seqomsuc  6471  oa1suc  6532  om1  6542  oe1  6544  oawordeulem  6554  oeoalem  6596  nnm1  6648  nnm2  6649  nneob  6652  omopthlem1  6655  mapsnconst  6815  mapsncnv  6816  map2xp  7033  cantnflt  7375  cnfcom2  7407  infxpenc  7647  infxpenc2  7651  ackbij1lem5  7852  alephom  8209  pwxpndom2  8289  adderpqlem  8580  addassnq  8584  mulcanenq  8586  distrnq  8587  ltanq  8597  ltexnq  8601  halfnq  8602  ltrnq  8605  archnq  8606  addclprlem2  8643  prlem934  8659  prlem936  8673  addcmpblnr  8696  mulcmpblnrlem  8697  ltsrpr  8701  m1p1sr  8716  m1m1sr  8717  0idsr  8721  1idsr  8722  00sr  8723  pn0sr  8725  recexsrlem  8727  mulgt0sr  8729  sqgt0sr  8730  mulresr  8763  axmulcom  8779  axmulass  8781  axdistr  8782  axi2m1  8783  ax1rid  8785  axcnre  8788  mul02lem1  8990  addid1  8994  add42i  9034  negid  9096  negsub  9097  subneg  9098  negsubdii  9133  muleqadd  9414  crne0  9741  2p2e4  9844  3p2e5  9857  3p3e6  9858  4p2e6  9859  4p3e7  9860  4p4e8  9861  5p2e7  9862  5p3e8  9863  5p4e9  9864  5p5e10  9865  6p2e8  9866  6p3e9  9867  6p4e10  9868  7p2e9  9869  7p3e10  9870  8p2e10  9871  3t3e9  9875  8th4div3  9937  halfpm6th  9938  addltmul  9949  nneo  10097  zeo  10099  numsuc  10138  numltc  10146  numsucc  10152  numma  10157  nummul1c  10162  6p5lem  10175  4t3lem  10197  decbin2  10230  xmulmnf1  10598  fztp  10843  fzprval  10846  fztpval  10847  fzshftral  10871  fzo01  10915  quoremz  10961  quoremnn0ALT  10963  intfrac2  10964  intfracq  10965  sqval  11165  sqrecii  11188  cu2  11203  i3  11206  i4  11207  binom2i  11214  binom3  11224  crreczi  11228  nn0opthlem1  11285  facp1  11295  faclbnd  11305  faclbnd2  11306  faclbnd4lem1  11308  faclbnd4lem4  11311  bcn1  11327  bcn2  11333  hashgadd  11361  hashxplem  11387  hashmap  11389  hashfun  11391  hashbclem  11392  fz1isolem  11401  ccatlid  11436  ccatrid  11437  eqs1  11449  wrdeqs1cat  11477  cats1un  11478  cats1fvn  11510  cats1cat  11513  swrds2  11562  reim0  11605  cji  11646  sqrm1  11763  absi  11773  rddif  11826  iseraltlem2  12157  iseralt  12159  fsump1i  12234  fsummulc2  12248  incexclem  12297  incexc  12298  arisum2  12321  geoihalfsum  12340  mertenslem1  12342  mertens  12344  ef0lem  12362  ege2le3  12373  eft0val  12394  ef4p  12395  efgt1p2  12396  efgt1p  12397  tanval2  12415  efival  12434  ef01bndlem  12466  sin01bnd  12467  cos01bnd  12468  cos1bnd  12469  cos2bnd  12470  rpnnen2lem11  12505  sqr2irrlem  12528  odd2np1lem  12588  odd2np1  12589  oddp1even  12591  divalglem5  12598  divalglem6  12599  bits0  12621  0bits  12632  bitsinv1lem  12634  gcdaddmlem  12709  3prm  12777  phiprm  12847  eulerthlem2  12852  prmdiv  12855  opoe  12866  pythagtriplem12  12881  pythagtriplem14  12883  pcmpt  12942  pcfac  12949  prmpwdvds  12953  pockthi  12956  prmreclem2  12966  prmreclem6  12970  4sqlem5  12991  4sqlem13  13006  modxai  13085  mod2xnegi  13088  gcdi  13090  decexp2  13092  numexpp1  13095  numexp2x  13096  decsplit0b  13097  decsplit1  13099  decsplit  13100  2exp6  13103  2exp16  13105  prmlem0  13109  139prm  13127  163prm  13128  317prm  13129  631prm  13130  1259lem1  13131  1259lem3  13133  1259lem4  13134  1259lem5  13135  1259prm  13136  2503lem1  13137  2503lem2  13138  2503lem3  13139  2503prm  13140  4001lem1  13141  4001lem2  13142  4001lem3  13143  4001lem4  13144  ressinbas  13206  rescfth  13813  xpccatid  13964  oduval  14236  oppgmnd  14829  lsmmod2  14987  efgi0  15031  efgi1  15032  efginvrel2  15038  efgsval2  15044  efgsp1  15048  efgredleme  15054  efgredlemc  15056  efgcpbllemb  15066  frgpnabllem1  15163  lt6abl  15183  gsumsn  15222  gsum2d  15225  pwsgsum  15232  dprd0  15268  dprdf1  15270  dprd2da  15279  ablfac1lem  15305  pgpfac1lem3  15314  pgpfaclem1  15318  opprrng  15415  mulgass3  15421  ply1assa  16280  ply1coe  16370  zlmval  16472  znbas  16499  znzrh2  16501  restin  16899  imacmp  17126  concompcon  17160  uptx  17321  cnpflf2  17697  tmdgsum2  17781  tsmsres  17828  tsmsf1o  17829  tsmsmhm  17830  prdsxmet  17935  resspwsds  17938  prdsxmslem2  18077  metdcn2  18346  metdcn  18347  metdscn2  18363  iimulcn  18438  icchmeo  18441  xrhmeo  18446  cnrehmeo  18453  cnheiborlem  18454  evth  18459  evth2  18460  lebnumlem2  18462  reparphti  18497  pcoass  18524  pi1xfrcnv  18557  ipcau2  18666  minveclem4  18798  pjthlem1  18803  ovolunlem1a  18857  unmbl  18897  uniioombl  18946  iblitg  19125  dfitg  19126  itg0  19136  iblcnlem1  19144  itgcnlem  19146  itgabs  19191  limcdif  19228  limccnp  19243  limccnp2  19244  dvexp  19304  dvmptid  19308  dvmptc  19309  dvmptfsum  19324  dveflem  19328  dvsincos  19330  mvth  19341  dvlipcn  19343  dvivthlem1  19357  dvfsumle  19370  dvfsumlem2  19376  itgsubst  19398  evlsval  19405  mpff  19427  tdeglem4  19448  tdeglem2  19449  plypf1  19596  plymullem1  19598  coesub  19640  dgrmulc  19654  fta1lem  19689  vieta1lem1  19692  vieta1lem2  19693  aalioulem4  19717  aaliou3lem3  19726  abelthlem2  19810  abelthlem8  19817  abelthlem9  19818  sinhalfpilem  19836  efhalfpi  19841  cospi  19842  efipi  19843  sin2pi  19845  cos2pi  19846  ef2pi  19847  sin2pim  19855  cos2pim  19856  sinmpi  19857  cosmpi  19858  sinppi  19859  cosppi  19860  sincosq4sgn  19871  tangtx  19875  sincos4thpi  19883  sincos6thpi  19885  sincos3rdpi  19886  pige3  19887  abssinper  19888  efif1olem4  19909  efifo  19911  eff1o  19913  logneg  19943  logimul  19970  logneg2  19971  dvrelog  19986  logcnlem4  19994  dvlog  20000  dvlog2  20002  logtayl  20009  1cxp  20021  ecxp  20022  cxpsqr  20052  dvsqr  20086  root1eq1  20097  cxpeq  20099  ang180lem1  20109  ang180lem2  20110  1cubrlem  20139  1cubr  20140  dcubic2  20142  mcubic  20145  cubic2  20146  binom4  20148  dquartlem1  20149  dquartlem2  20150  dquart  20151  quart1lem  20153  quart1  20154  quartlem1  20155  asinsin  20190  asin1  20192  acos1  20193  atanlogsublem  20213  atanlogsub  20214  efiatan2  20215  2efiatan  20216  tanatan  20217  atanbnd  20224  atan1  20226  dvatan  20233  atantayl2  20236  leibpilem2  20239  leibpi  20240  log2cnv  20242  log2tlbnd  20243  log2ublem1  20244  log2ublem2  20245  log2ublem3  20246  log2ub  20247  birthday  20251  amgmlem  20286  emcllem5  20295  wilthlem2  20309  ftalem6  20317  basellem2  20321  basellem3  20322  basellem5  20324  basellem8  20327  cht1  20405  chp1  20407  1sgmprm  20440  ppiublem2  20444  ppiub  20445  chtublem  20452  chtub  20453  logfacbnd3  20464  bcp1ctr  20520  bclbnd  20521  bposlem1  20525  bposlem4  20528  bposlem6  20530  bposlem8  20532  bposlem9  20533  lgslem1  20537  lgsdir2lem1  20564  lgsdir2lem2  20565  lgsdir2lem3  20566  lgsdir2lem5  20568  lgs1  20579  lgseisenlem1  20590  lgseisenlem3  20592  lgsquadlem1  20595  lgsquadlem2  20596  lgsquad2lem2  20600  m1lgs  20603  2sqlem8  20613  2sqblem  20618  logdivsum  20684  mulog2sumlem2  20686  log2sumbnd  20695  selberglem1  20696  selberglem2  20697  pntrmax  20715  pntibndlem2  20742  pntibndlem3  20743  pntlemg  20749  pntlemr  20753  pntlemo  20758  ostth2lem3  20786  ostth2lem4  20787  smcnlem  21272  ipidsq  21288  dipcj  21292  dip0r  21295  nmlnoubi  21376  nmblolbii  21379  blocnilem  21384  ip1ilem  21406  ip2i  21408  ipdirilem  21409  ipasslem10  21419  ipasslem11  21420  siilem1  21431  hvmul0  21605  hvsubsub4i  21640  hvnegdii  21643  hvsubeq0i  21644  hvsubcan2i  21645  hvsubaddi  21647  hvsub0  21657  hisubcomi  21685  normlem0  21690  normlem1  21691  normlem2  21692  normlem3  21693  normlem9  21699  norm-ii-i  21718  norm3difi  21728  normpari  21735  polid2i  21738  polidi  21739  bcsiALT  21760  pjhthlem1  21972  chdmm3i  22060  chdmm4i  22061  chjidm  22101  chj4i  22104  chjjdiri  22105  spanunsni  22160  pjoml4i  22168  cmcm2i  22174  qlax4i  22211  qlax5i  22212  pjadjii  22255  pjmulii  22258  pjsubii  22259  pjssmii  22262  pjcji  22265  pjneli  22304  hoadd32i  22360  ho0subi  22377  hosubid1  22380  hosd2i  22405  hopncani  22406  hosubeq0i  22408  lnopeq0lem1  22587  lnopunilem1  22592  lnophmlem2  22599  nmbdoplbi  22606  nmcopexi  22609  lnfnmuli  22626  nmcfnexi  22633  nmoptri2i  22681  nmopcoadji  22683  golem1  22853  mdsl1i  22903  cvmdi  22906  mdslmd3i  22914  csmdsymi  22916  ballotlem2  23049  ballotth  23098  raddcn  23304  xrge00  23313  xrge0iifhom  23321  xrge0mulc1cn  23325  gsumconstf  23383  cbvesum  23424  esumpfinvallem  23444  esumpfinvalf  23446  dya2iocseg  23581  coinflipprob  23682  coinflippvt  23687  subfacp1lem1  23712  subfacp1lem5  23717  subfacval2  23720  subfaclim  23721  subfacval3  23722  cvxpcon  23775  cvxscon  23776  vdgr1c  23898  vdegp1ai  23910  vdegp1bi  23911  vdegp1ci  23912  sinccvglem  24007  4bc3eq4  24100  4bc2eq6  24101  frrlem5  24287  ax5seglem7  24565  axlowdimlem4  24575  axlowdimlem16  24587  bpoly0  24787  bpoly1  24788  bpolydiflem  24791  bpoly2  24794  bpoly3  24795  bpoly4  24796  fsumcube  24797  dvreasin  24925  areacirclem2  24936  areacirclem5  24940  areacirc  24942  geme2  25286  nfwpr4c  25296  tolat  25297  fprodp1fi  25339  limfilnei  25572  1cat  25770  dualcat2  25795  isntr  25884  intset  26055  fnckle  26056  prdstotbnd  26529  prdsbnd2  26530  repwsmet  26569  rrnequiv  26570  reheibor  26574  mapfzcons  26804  mapfzcons1cl  26806  2rexfrabdioph  26888  3rexfrabdioph  26889  4rexfrabdioph  26890  6rexfrabdioph  26891  7rexfrabdioph  26892  rabdiophlem2  26894  diophren  26907  rabren3dioph  26909  pellexlem5  26929  pell1qr1  26967  rmspecfund  27005  jm2.17a  27058  jm2.17b  27059  jm2.27c  27111  jm2.27dlem5  27117  lmhmlnmsplit  27196  dsmmval2  27213  psgnunilem2  27429  psgnunilem4  27431  psgnpmtr  27444  lhe4.4ex1a  27557  expgrowthi  27561  expgrowth  27563  refsumcn  27712  m1expeven  27736  dvcosre  27752  itgsin0pilem1  27755  itgsinexplem1  27759  stoweidlem13  27773  wallispilem4  27828  wallispi2lem1  27831  wallispi2lem2  27832  stirlinglem1  27834  sec0  28241  elogb  28270  dalem-cly  29933  pmodN  30112  cdleme0cp  30476  cdleme0cq  30477  cdleme1  30489  cdleme3d  30493  cdleme3h  30497  cdleme4  30500  cdleme5  30502  cdleme7a  30505  cdleme8  30512  cdleme9  30515  cdleme10  30516  cdleme11g  30527  cdleme15b  30537  cdleme21  30599  cdleme22e  30606  cdleme22eALTN  30607  cdleme23c  30613  cdleme25cv  30620  cdleme35b  30712  cdleme35c  30713  cdleme42a  30733  cdleme42d  30735  cdleme43aN  30751  cdlemeg46gfv  30792  cdlemk35  31174  dihjatcclem1  31681  lcdval2  31853  mapdpglem21  31955
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1637  ax-8 1645  ax-6 1705  ax-7 1710  ax-11 1717  ax-12 1868  ax-ext 2266
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1531  df-nf 1534  df-sb 1632  df-clab 2272  df-cleq 2278  df-clel 2281  df-nfc 2410  df-rex 2551  df-rab 2554  df-v 2792  df-dif 3157  df-un 3159  df-in 3161  df-ss 3168  df-nul 3458  df-if 3568  df-sn 3648  df-pr 3649  df-op 3651  df-uni 3830  df-br 4026  df-iota 5221  df-fv 5265  df-ov 5863
  Copyright terms: Public domain W3C validator