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

Theorem oveq2i 5869
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 5866 . 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 1623  (class class class)co 5858
This theorem is referenced by:  caov32  6047  caov4  6051  caov42  6053  seqomsuc  6469  oa1suc  6530  om1  6540  oe1  6542  oawordeulem  6552  oeoalem  6594  nnm1  6646  nnm2  6647  nneob  6650  omopthlem1  6653  mapsnconst  6813  mapsncnv  6814  map2xp  7031  cantnflt  7373  cnfcom2  7405  infxpenc  7645  infxpenc2  7649  ackbij1lem5  7850  alephom  8207  pwxpndom2  8287  adderpqlem  8578  addassnq  8582  mulcanenq  8584  distrnq  8585  ltanq  8595  ltexnq  8599  halfnq  8600  ltrnq  8603  archnq  8604  addclprlem2  8641  prlem934  8657  prlem936  8671  addcmpblnr  8694  mulcmpblnrlem  8695  ltsrpr  8699  m1p1sr  8714  m1m1sr  8715  0idsr  8719  1idsr  8720  00sr  8721  pn0sr  8723  recexsrlem  8725  mulgt0sr  8727  sqgt0sr  8728  mulresr  8761  axmulcom  8777  axmulass  8779  axdistr  8780  axi2m1  8781  ax1rid  8783  axcnre  8786  mul02lem1  8988  addid1  8992  add42i  9032  negid  9094  negsub  9095  subneg  9096  negsubdii  9131  muleqadd  9412  crne0  9739  2p2e4  9842  3p2e5  9855  3p3e6  9856  4p2e6  9857  4p3e7  9858  4p4e8  9859  5p2e7  9860  5p3e8  9861  5p4e9  9862  5p5e10  9863  6p2e8  9864  6p3e9  9865  6p4e10  9866  7p2e9  9867  7p3e10  9868  8p2e10  9869  3t3e9  9873  8th4div3  9935  halfpm6th  9936  addltmul  9947  nneo  10095  zeo  10097  numsuc  10136  numltc  10144  numsucc  10150  numma  10155  nummul1c  10160  6p5lem  10173  4t3lem  10195  decbin2  10228  xmulmnf1  10596  fztp  10841  fzprval  10844  fztpval  10845  fzshftral  10869  fzo01  10913  quoremz  10959  quoremnn0ALT  10961  intfrac2  10962  intfracq  10963  sqval  11163  sqrecii  11186  cu2  11201  i3  11204  i4  11205  binom2i  11212  binom3  11222  crreczi  11226  nn0opthlem1  11283  facp1  11293  faclbnd  11303  faclbnd2  11304  faclbnd4lem1  11306  faclbnd4lem4  11309  bcn1  11325  bcn2  11331  hashgadd  11359  hashxplem  11385  hashmap  11387  hashfun  11389  hashbclem  11390  fz1isolem  11399  ccatlid  11434  ccatrid  11435  eqs1  11447  wrdeqs1cat  11475  cats1un  11476  cats1fvn  11508  cats1cat  11511  swrds2  11560  reim0  11603  cji  11644  sqrm1  11761  absi  11771  rddif  11824  iseraltlem2  12155  iseralt  12157  fsump1i  12232  fsummulc2  12246  incexclem  12295  incexc  12296  arisum2  12319  geoihalfsum  12338  mertenslem1  12340  mertens  12342  ef0lem  12360  ege2le3  12371  eft0val  12392  ef4p  12393  efgt1p2  12394  efgt1p  12395  tanval2  12413  efival  12432  ef01bndlem  12464  sin01bnd  12465  cos01bnd  12466  cos1bnd  12467  cos2bnd  12468  rpnnen2lem11  12503  sqr2irrlem  12526  odd2np1lem  12586  odd2np1  12587  oddp1even  12589  divalglem5  12596  divalglem6  12597  bits0  12619  0bits  12630  bitsinv1lem  12632  gcdaddmlem  12707  3prm  12775  phiprm  12845  eulerthlem2  12850  prmdiv  12853  opoe  12864  pythagtriplem12  12879  pythagtriplem14  12881  pcmpt  12940  pcfac  12947  prmpwdvds  12951  pockthi  12954  prmreclem2  12964  prmreclem6  12968  4sqlem5  12989  4sqlem13  13004  modxai  13083  mod2xnegi  13086  gcdi  13088  decexp2  13090  numexpp1  13093  numexp2x  13094  decsplit0b  13095  decsplit1  13097  decsplit  13098  2exp6  13101  2exp16  13103  prmlem0  13107  139prm  13125  163prm  13126  317prm  13127  631prm  13128  1259lem1  13129  1259lem3  13131  1259lem4  13132  1259lem5  13133  1259prm  13134  2503lem1  13135  2503lem2  13136  2503lem3  13137  2503prm  13138  4001lem1  13139  4001lem2  13140  4001lem3  13141  4001lem4  13142  ressinbas  13204  rescfth  13811  xpccatid  13962  oduval  14234  oppgmnd  14827  lsmmod2  14985  efgi0  15029  efgi1  15030  efginvrel2  15036  efgsval2  15042  efgsp1  15046  efgredleme  15052  efgredlemc  15054  efgcpbllemb  15064  frgpnabllem1  15161  lt6abl  15181  gsumsn  15220  gsum2d  15223  pwsgsum  15230  dprd0  15266  dprdf1  15268  dprd2da  15277  ablfac1lem  15303  pgpfac1lem3  15312  pgpfaclem1  15316  opprrng  15413  mulgass3  15419  ply1assa  16278  ply1coe  16368  zlmval  16470  znbas  16497  znzrh2  16499  restin  16897  imacmp  17124  concompcon  17158  uptx  17319  cnpflf2  17695  tmdgsum2  17779  tsmsres  17826  tsmsf1o  17827  tsmsmhm  17828  prdsxmet  17933  resspwsds  17936  prdsxmslem2  18075  metdcn2  18344  metdcn  18345  metdscn2  18361  iimulcn  18436  icchmeo  18439  xrhmeo  18444  cnrehmeo  18451  cnheiborlem  18452  evth  18457  evth2  18458  lebnumlem2  18460  reparphti  18495  pcoass  18522  pi1xfrcnv  18555  ipcau2  18664  minveclem4  18796  pjthlem1  18801  ovolunlem1a  18855  unmbl  18895  uniioombl  18944  iblitg  19123  dfitg  19124  itg0  19134  iblcnlem1  19142  itgcnlem  19144  itgabs  19189  limcdif  19226  limccnp  19241  limccnp2  19242  dvexp  19302  dvmptid  19306  dvmptc  19307  dvmptfsum  19322  dveflem  19326  dvsincos  19328  mvth  19339  dvlipcn  19341  dvivthlem1  19355  dvfsumle  19368  dvfsumlem2  19374  itgsubst  19396  evlsval  19403  mpff  19425  tdeglem4  19446  tdeglem2  19447  plypf1  19594  plymullem1  19596  coesub  19638  dgrmulc  19652  fta1lem  19687  vieta1lem1  19690  vieta1lem2  19691  aalioulem4  19715  aaliou3lem3  19724  abelthlem2  19808  abelthlem8  19815  abelthlem9  19816  sinhalfpilem  19834  efhalfpi  19839  cospi  19840  efipi  19841  sin2pi  19843  cos2pi  19844  ef2pi  19845  sin2pim  19853  cos2pim  19854  sinmpi  19855  cosmpi  19856  sinppi  19857  cosppi  19858  sincosq4sgn  19869  tangtx  19873  sincos4thpi  19881  sincos6thpi  19883  sincos3rdpi  19884  pige3  19885  abssinper  19886  efif1olem4  19907  efifo  19909  eff1o  19911  logneg  19941  logimul  19968  logneg2  19969  dvrelog  19984  logcnlem4  19992  dvlog  19998  dvlog2  20000  logtayl  20007  1cxp  20019  ecxp  20020  cxpsqr  20050  dvsqr  20084  root1eq1  20095  cxpeq  20097  ang180lem1  20107  ang180lem2  20108  1cubrlem  20137  1cubr  20138  dcubic2  20140  mcubic  20143  cubic2  20144  binom4  20146  dquartlem1  20147  dquartlem2  20148  dquart  20149  quart1lem  20151  quart1  20152  quartlem1  20153  asinsin  20188  asin1  20190  acos1  20191  atanlogsublem  20211  atanlogsub  20212  efiatan2  20213  2efiatan  20214  tanatan  20215  atanbnd  20222  atan1  20224  dvatan  20231  atantayl2  20234  leibpilem2  20237  leibpi  20238  log2cnv  20240  log2tlbnd  20241  log2ublem1  20242  log2ublem2  20243  log2ublem3  20244  log2ub  20245  birthday  20249  amgmlem  20284  emcllem5  20293  wilthlem2  20307  ftalem6  20315  basellem2  20319  basellem3  20320  basellem5  20322  basellem8  20325  cht1  20403  chp1  20405  1sgmprm  20438  ppiublem2  20442  ppiub  20443  chtublem  20450  chtub  20451  logfacbnd3  20462  bcp1ctr  20518  bclbnd  20519  bposlem1  20523  bposlem4  20526  bposlem6  20528  bposlem8  20530  bposlem9  20531  lgslem1  20535  lgsdir2lem1  20562  lgsdir2lem2  20563  lgsdir2lem3  20564  lgsdir2lem5  20566  lgs1  20577  lgseisenlem1  20588  lgseisenlem3  20590  lgsquadlem1  20593  lgsquadlem2  20594  lgsquad2lem2  20598  m1lgs  20601  2sqlem8  20611  2sqblem  20616  logdivsum  20682  mulog2sumlem2  20684  log2sumbnd  20693  selberglem1  20694  selberglem2  20695  pntrmax  20713  pntibndlem2  20740  pntibndlem3  20741  pntlemg  20747  pntlemr  20751  pntlemo  20756  ostth2lem3  20784  ostth2lem4  20785  smcnlem  21270  ipidsq  21286  dipcj  21290  dip0r  21293  nmlnoubi  21374  nmblolbii  21377  blocnilem  21382  ip1ilem  21404  ip2i  21406  ipdirilem  21407  ipasslem10  21417  ipasslem11  21418  siilem1  21429  hvmul0  21603  hvsubsub4i  21638  hvnegdii  21641  hvsubeq0i  21642  hvsubcan2i  21643  hvsubaddi  21645  hvsub0  21655  hisubcomi  21683  normlem0  21688  normlem1  21689  normlem2  21690  normlem3  21691  normlem9  21697  norm-ii-i  21716  norm3difi  21726  normpari  21733  polid2i  21736  polidi  21737  bcsiALT  21758  pjhthlem1  21970  chdmm3i  22058  chdmm4i  22059  chjidm  22099  chj4i  22102  chjjdiri  22103  spanunsni  22158  pjoml4i  22166  cmcm2i  22172  qlax4i  22209  qlax5i  22210  pjadjii  22253  pjmulii  22256  pjsubii  22257  pjssmii  22260  pjcji  22263  pjneli  22302  hoadd32i  22358  ho0subi  22375  hosubid1  22378  hosd2i  22403  hopncani  22404  hosubeq0i  22406  lnopeq0lem1  22585  lnopunilem1  22590  lnophmlem2  22597  nmbdoplbi  22604  nmcopexi  22607  lnfnmuli  22624  nmcfnexi  22631  nmoptri2i  22679  nmopcoadji  22681  golem1  22851  mdsl1i  22901  cvmdi  22904  mdslmd3i  22912  csmdsymi  22914  ballotlem2  23047  ballotth  23096  raddcn  23302  xrge00  23311  xrge0iifhom  23319  xrge0mulc1cn  23323  gsumconstf  23381  cbvesum  23422  esumpfinvallem  23442  esumpfinvalf  23444  dya2iocseg  23579  coinflipprob  23680  coinflippvt  23685  subfacp1lem1  23710  subfacp1lem5  23715  subfacval2  23718  subfaclim  23719  subfacval3  23720  cvxpcon  23773  cvxscon  23774  vdgr1c  23896  vdegp1ai  23908  vdegp1bi  23909  vdegp1ci  23910  sinccvglem  24005  4bc3eq4  24098  4bc2eq6  24099  frrlem5  24285  ax5seglem7  24563  axlowdimlem4  24573  axlowdimlem16  24585  bpoly0  24785  bpoly1  24786  bpolydiflem  24789  bpoly2  24792  bpoly3  24793  bpoly4  24794  fsumcube  24795  dvreasin  24923  areacirclem2  24925  areacirclem5  24929  areacirc  24931  geme2  25275  nfwpr4c  25285  tolat  25286  fprodp1fi  25328  limfilnei  25561  1cat  25759  dualcat2  25784  isntr  25873  intset  26044  fnckle  26045  prdstotbnd  26518  prdsbnd2  26519  repwsmet  26558  rrnequiv  26559  reheibor  26563  mapfzcons  26793  mapfzcons1cl  26795  2rexfrabdioph  26877  3rexfrabdioph  26878  4rexfrabdioph  26879  6rexfrabdioph  26880  7rexfrabdioph  26881  rabdiophlem2  26883  diophren  26896  rabren3dioph  26898  pellexlem5  26918  pell1qr1  26956  rmspecfund  26994  jm2.17a  27047  jm2.17b  27048  jm2.27c  27100  jm2.27dlem5  27106  lmhmlnmsplit  27185  dsmmval2  27202  psgnunilem2  27418  psgnunilem4  27420  psgnpmtr  27433  lhe4.4ex1a  27546  expgrowthi  27550  expgrowth  27552  refsumcn  27701  m1expeven  27725  dvcosre  27741  itgsin0pilem1  27744  itgsinexplem1  27748  stoweidlem13  27762  wallispilem4  27817  wallispi2lem1  27820  wallispi2lem2  27821  stirlinglem1  27823  sec0  28230  dalem-cly  29860  pmodN  30039  cdleme0cp  30403  cdleme0cq  30404  cdleme1  30416  cdleme3d  30420  cdleme3h  30424  cdleme4  30427  cdleme5  30429  cdleme7a  30432  cdleme8  30439  cdleme9  30442  cdleme10  30443  cdleme11g  30454  cdleme15b  30464  cdleme21  30526  cdleme22e  30533  cdleme22eALTN  30534  cdleme23c  30540  cdleme25cv  30547  cdleme35b  30639  cdleme35c  30640  cdleme42a  30660  cdleme42d  30662  cdleme43aN  30678  cdlemeg46gfv  30719  cdlemk35  31101  dihjatcclem1  31608  lcdval2  31780  mapdpglem21  31882
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-rex 2549  df-rab 2552  df-v 2790  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-sn 3646  df-pr 3647  df-op 3649  df-uni 3828  df-br 4024  df-iota 5219  df-fv 5263  df-ov 5861
  Copyright terms: Public domain W3C validator