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

Theorem oveq2i 6092
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 6089 . 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 1652  (class class class)co 6081
This theorem is referenced by:  caov32  6274  caov4  6278  caov42  6280  seqomsuc  6714  oa1suc  6775  om1  6785  oe1  6787  oawordeulem  6797  oeoalem  6839  nnm1  6891  nnm2  6892  nneob  6895  omopthlem1  6898  mapsnconst  7059  mapsncnv  7060  map2xp  7277  cantnflt  7627  cnfcom2  7659  infxpenc  7899  infxpenc2  7903  ackbij1lem5  8104  alephom  8460  pwxpndom2  8540  adderpqlem  8831  addassnq  8835  mulcanenq  8837  distrnq  8838  ltanq  8848  ltexnq  8852  halfnq  8853  ltrnq  8856  archnq  8857  addclprlem2  8894  prlem934  8910  prlem936  8924  addcmpblnr  8947  mulcmpblnrlem  8948  ltsrpr  8952  m1p1sr  8967  m1m1sr  8968  0idsr  8972  1idsr  8973  00sr  8974  pn0sr  8976  recexsrlem  8978  mulgt0sr  8980  sqgt0sr  8981  mulresr  9014  axmulcom  9030  axmulass  9032  axdistr  9033  axi2m1  9034  ax1rid  9036  axcnre  9039  mul02lem1  9242  addid1  9246  add42i  9286  negid  9348  negsub  9349  subneg  9350  negsubdii  9385  muleqadd  9666  crne0  9993  2p2e4  10098  3p2e5  10111  3p3e6  10112  4p2e6  10113  4p3e7  10114  4p4e8  10115  5p2e7  10116  5p3e8  10117  5p4e9  10118  5p5e10  10119  6p2e8  10120  6p3e9  10121  6p4e10  10122  7p2e9  10123  7p3e10  10124  8p2e10  10125  3t3e9  10129  8th4div3  10191  halfpm6th  10192  addltmul  10203  nn0n0n1ge2  10280  nneo  10353  zeo  10355  numsuc  10394  numltc  10402  numsucc  10408  numma  10413  nummul1c  10418  6p5lem  10431  4t3lem  10453  decbin2  10486  xmulmnf1  10855  fztp  11102  fz0tp  11103  fzprval  11106  fztpval  11107  fzshftral  11134  fzo01  11182  fzo12sn  11183  fzo0to2pr  11184  fzo0to3tp  11185  fzo0to42pr  11186  quoremz  11236  quoremnn0ALT  11238  intfrac2  11239  intfracq  11240  sqval  11441  sqrecii  11464  cu2  11479  i3  11482  i4  11483  binom2i  11490  binom3  11500  crreczi  11504  nn0opthlem1  11561  facp1  11571  faclbnd  11581  faclbnd2  11582  faclbnd4lem1  11584  faclbnd4lem4  11587  bcn1  11604  bcn2  11610  hashgadd  11651  hashxplem  11696  hashmap  11698  hashfun  11700  hashbclem  11701  fz1isolem  11710  ccatlid  11748  ccatrid  11749  eqs1  11761  wrdeqs1cat  11789  cats1un  11790  cats1fvn  11822  cats1cat  11825  swrds2  11880  reim0  11923  cji  11964  sqrm1  12081  absi  12091  rddif  12144  iseraltlem2  12476  iseralt  12478  fsump1i  12553  fsummulc2  12567  incexclem  12616  incexc  12617  arisum2  12640  geoihalfsum  12659  mertenslem1  12661  mertens  12663  ef0lem  12681  ege2le3  12692  eft0val  12713  ef4p  12714  efgt1p2  12715  efgt1p  12716  tanval2  12734  efival  12753  ef01bndlem  12785  sin01bnd  12786  cos01bnd  12787  cos1bnd  12788  cos2bnd  12789  rpnnen2lem11  12824  sqr2irrlem  12847  odd2np1lem  12907  odd2np1  12908  oddp1even  12910  divalglem5  12917  divalglem6  12918  bits0  12940  0bits  12951  gcdaddmlem  13028  3prm  13096  phiprm  13166  eulerthlem2  13171  prmdiv  13174  opoe  13185  pythagtriplem12  13200  pythagtriplem14  13202  pcmpt  13261  pcfac  13268  prmpwdvds  13272  pockthi  13275  prmreclem2  13285  prmreclem6  13289  4sqlem5  13310  4sqlem13  13325  modxai  13404  mod2xnegi  13407  gcdi  13409  decexp2  13411  numexpp1  13414  numexp2x  13415  decsplit0b  13416  decsplit1  13418  decsplit  13419  2exp6  13422  2exp16  13424  prmlem0  13428  139prm  13446  163prm  13447  317prm  13448  631prm  13449  1259lem1  13450  1259lem3  13452  1259lem4  13453  1259lem5  13454  1259prm  13455  2503lem1  13456  2503lem2  13457  2503lem3  13458  2503prm  13459  4001lem1  13460  4001lem2  13461  4001lem3  13462  4001lem4  13463  ressinbas  13525  rescfth  14134  xpccatid  14285  oduval  14557  oppgmnd  15150  lsmmod2  15308  efgi0  15352  efgi1  15353  efginvrel2  15359  efgsval2  15365  efgsp1  15369  efgredleme  15375  efgredlemc  15377  efgcpbllemb  15387  frgpnabllem1  15484  lt6abl  15504  gsumsn  15543  gsum2d  15546  pwsgsum  15553  dprd0  15589  dprdf1  15591  dprd2da  15600  ablfac1lem  15626  pgpfac1lem3  15635  pgpfaclem1  15639  opprrng  15736  mulgass3  15742  ply1assa  16597  ply1coe  16684  zlmval  16797  znbas  16824  znzrh2  16826  restin  17230  imacmp  17460  concompcon  17495  uptx  17657  cnpflf2  18032  tmdgsum2  18126  tsmsres  18173  tsmsf1o  18174  tsmsmhm  18175  prdsxmet  18399  resspwsds  18402  prdsxmslem2  18559  metdcn2  18870  metdcn  18871  metdscn2  18887  iimulcn  18963  icchmeo  18966  xrhmeo  18971  cnrehmeo  18978  cnheiborlem  18979  evth  18984  evth2  18985  lebnumlem2  18987  reparphti  19022  pcoass  19049  pi1xfrcnv  19082  ipcau2  19191  minveclem4  19333  pjthlem1  19338  ovolunlem1a  19392  unmbl  19432  uniioombl  19481  iblitg  19660  dfitg  19661  itg0  19671  iblcnlem1  19679  itgcnlem  19681  itgabs  19726  limcdif  19763  limccnp  19778  limccnp2  19779  dvexp  19839  dvmptid  19843  dvmptc  19844  dvmptfsum  19859  dveflem  19863  dvsincos  19865  mvth  19876  dvlipcn  19878  dvivthlem1  19892  dvfsumle  19905  dvfsumlem2  19911  itgsubst  19933  evlsval  19940  mpff  19962  tdeglem4  19983  tdeglem2  19984  plypf1  20131  plymullem1  20133  coesub  20175  dgrmulc  20189  fta1lem  20224  vieta1lem1  20227  vieta1lem2  20228  aalioulem4  20252  aaliou3lem3  20261  abelthlem2  20348  abelthlem8  20355  abelthlem9  20356  sinhalfpilem  20374  efhalfpi  20379  cospi  20380  efipi  20381  sin2pi  20383  cos2pi  20384  ef2pi  20385  sin2pim  20393  cos2pim  20394  sinmpi  20395  cosmpi  20396  sinppi  20397  cosppi  20398  sincosq4sgn  20409  tangtx  20413  sincos4thpi  20421  sincos6thpi  20423  sincos3rdpi  20424  pige3  20425  abssinper  20426  efif1olem4  20447  efifo  20449  eff1o  20451  logneg  20482  logimul  20509  logneg2  20510  dvrelog  20528  logcnlem4  20536  dvlog  20542  dvlog2  20544  logtayl  20551  1cxp  20563  ecxp  20564  cxpsqr  20594  dvsqr  20628  root1eq1  20639  cxpeq  20641  ang180lem1  20651  ang180lem2  20652  1cubrlem  20681  1cubr  20682  dcubic2  20684  mcubic  20687  cubic2  20688  binom4  20690  dquartlem1  20691  dquartlem2  20692  dquart  20693  quart1lem  20695  quart1  20696  quartlem1  20697  asinsin  20732  asin1  20734  acos1  20735  atanlogsublem  20755  atanlogsub  20756  efiatan2  20757  2efiatan  20758  tanatan  20759  atanbnd  20766  atan1  20768  dvatan  20775  atantayl2  20778  leibpilem2  20781  leibpi  20782  log2cnv  20784  log2tlbnd  20785  log2ublem1  20786  log2ublem2  20787  log2ublem3  20788  log2ub  20789  birthday  20793  amgmlem  20828  emcllem5  20838  wilthlem2  20852  ftalem6  20860  basellem2  20864  basellem3  20865  basellem5  20867  basellem8  20870  cht1  20948  chp1  20950  1sgmprm  20983  ppiublem2  20987  ppiub  20988  chtublem  20995  chtub  20996  logfacbnd3  21007  bcp1ctr  21063  bclbnd  21064  bposlem1  21068  bposlem4  21071  bposlem6  21073  bposlem8  21075  bposlem9  21076  lgslem1  21080  lgsdir2lem1  21107  lgsdir2lem2  21108  lgsdir2lem3  21109  lgsdir2lem5  21111  lgs1  21122  lgseisenlem1  21133  lgseisenlem3  21135  lgsquadlem1  21138  lgsquadlem2  21139  lgsquad2lem2  21143  m1lgs  21146  2sqlem8  21156  2sqblem  21161  logdivsum  21227  mulog2sumlem2  21229  log2sumbnd  21238  selberglem1  21239  selberglem2  21240  pntrmax  21258  pntibndlem2  21285  pntibndlem3  21286  pntlemg  21292  pntlemr  21296  pntlemo  21301  ostth2lem3  21329  ostth2lem4  21330  0wlk  21545  0trl  21546  wlkntrllem2  21560  wlkntrl  21562  constr1trl  21588  1pthonlem1  21589  constr2wlk  21598  constr2trl  21599  wlkdvspthlem  21607  constr3trllem3  21639  constr3trllem4  21640  constr3trllem5  21641  constr3pthlem1  21642  constr3pthlem3  21644  vdgr1c  21676  vdegp1ai  21706  vdegp1bi  21707  vdegp1ci  21708  smcnlem  22193  ipidsq  22209  dipcj  22213  dip0r  22216  nmlnoubi  22297  nmblolbii  22300  blocnilem  22305  ip1ilem  22327  ip2i  22329  ipdirilem  22330  ipasslem10  22340  ipasslem11  22341  siilem1  22352  hvmul0  22526  hvsubsub4i  22561  hvnegdii  22564  hvsubeq0i  22565  hvsubcan2i  22566  hvsubaddi  22568  hvsub0  22578  hisubcomi  22606  normlem0  22611  normlem1  22612  normlem2  22613  normlem3  22614  normlem9  22620  norm-ii-i  22639  norm3difi  22649  normpari  22656  polid2i  22659  polidi  22660  bcsiALT  22681  pjhthlem1  22893  chdmm3i  22981  chdmm4i  22982  chjidm  23022  chj4i  23025  chjjdiri  23026  spanunsni  23081  pjoml4i  23089  cmcm2i  23095  qlax4i  23132  qlax5i  23133  pjadjii  23176  pjmulii  23179  pjsubii  23180  pjssmii  23183  pjcji  23186  pjneli  23225  hoadd32i  23281  ho0subi  23298  hosubid1  23301  hosd2i  23326  hopncani  23327  hosubeq0i  23329  lnopeq0lem1  23508  lnopunilem1  23513  lnophmlem2  23520  nmbdoplbi  23527  nmcopexi  23530  lnfnmuli  23547  nmcfnexi  23554  nmoptri2i  23602  nmopcoadji  23604  golem1  23774  mdsl1i  23824  cvmdi  23827  mdslmd3i  23835  csmdsymi  23837  xrge00  24208  gsumconstf  24222  raddcn  24315  xrge0iifhom  24323  xrge0mulc1cn  24327  cbvesum  24438  gsumesum  24451  esumpfinvallem  24464  esumpfinvalf  24466  dya2icoseg  24627  orrvcval4  24722  orrvcoel  24723  orrvccel  24724  coinflipprob  24737  coinflippvt  24742  ballotlem2  24746  ballotth  24795  lgamgulmlem2  24814  lgamgulmlem5  24817  lgam1  24848  subfacp1lem1  24865  subfacp1lem5  24870  subfacval2  24873  subfaclim  24874  subfacval3  24875  cvxpcon  24929  cvxscon  24930  sinccvglem  25109  4bc3eq4  25203  4bc2eq6  25204  risefall0lem  25342  risefac1  25349  fallfac1  25350  fallfacfwd  25352  faclimlem1  25362  frrlem5  25586  ax5seglem7  25874  axlowdimlem4  25884  axlowdimlem16  25896  bpoly0  26096  bpoly1  26097  bpolydiflem  26100  bpoly2  26103  bpoly3  26104  bpoly4  26105  fsumcube  26106  itgabsnc  26274  ftc1anclem8  26287  dvreasin  26290  areacirclem1  26292  areacirclem4  26295  areacirc  26297  prdstotbnd  26503  prdsbnd2  26504  repwsmet  26543  rrnequiv  26544  reheibor  26548  mapfzcons  26772  mapfzcons1cl  26774  2rexfrabdioph  26856  3rexfrabdioph  26857  4rexfrabdioph  26858  6rexfrabdioph  26859  7rexfrabdioph  26860  rabdiophlem2  26862  diophren  26874  rabren3dioph  26876  pellexlem5  26896  pell1qr1  26934  rmspecfund  26972  jm2.17a  27025  jm2.17b  27026  jm2.27c  27078  jm2.27dlem5  27084  lmhmlnmsplit  27162  dsmmval2  27179  psgnunilem2  27395  psgnunilem4  27397  psgnpmtr  27410  lhe4.4ex1a  27523  expgrowthi  27527  expgrowth  27529  refsumcn  27677  m1expeven  27701  dvcosre  27717  itgsin0pilem1  27720  itgsinexplem1  27724  stoweidlem13  27738  wallispilem4  27793  wallispi2lem1  27796  wallispi2lem2  27797  stirlinglem1  27799  f13idfv  28082  swrdccatin12lem4  28213  swrdccat3a  28217  lstccats1fst  28263  sec0  28503  elogb  28532  dalem-cly  30468  pmodN  30647  cdleme0cp  31011  cdleme0cq  31012  cdleme1  31024  cdleme3d  31028  cdleme3h  31032  cdleme4  31035  cdleme5  31037  cdleme7a  31040  cdleme8  31047  cdleme9  31050  cdleme10  31051  cdleme11g  31062  cdleme15b  31072  cdleme21  31134  cdleme22e  31141  cdleme22eALTN  31142  cdleme23c  31148  cdleme25cv  31155  cdleme35b  31247  cdleme35c  31248  cdleme42a  31268  cdleme42d  31270  cdleme43aN  31286  cdlemeg46gfv  31327  cdlemk35  31709  dihjatcclem1  32216  lcdval2  32388  mapdpglem21  32490
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2423  df-cleq 2429  df-clel 2432  df-nfc 2561  df-rex 2711  df-rab 2714  df-v 2958  df-dif 3323  df-un 3325  df-in 3327  df-ss 3334  df-nul 3629  df-if 3740  df-sn 3820  df-pr 3821  df-op 3823  df-uni 4016  df-br 4213  df-iota 5418  df-fv 5462  df-ov 6084
  Copyright terms: Public domain W3C validator