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

Theorem oveq2i 5992
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 5989 . 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 1647  (class class class)co 5981
This theorem is referenced by:  caov32  6174  caov4  6178  caov42  6180  seqomsuc  6611  oa1suc  6672  om1  6682  oe1  6684  oawordeulem  6694  oeoalem  6736  nnm1  6788  nnm2  6789  nneob  6792  omopthlem1  6795  mapsnconst  6956  mapsncnv  6957  map2xp  7174  cantnflt  7520  cnfcom2  7552  infxpenc  7792  infxpenc2  7796  ackbij1lem5  7997  alephom  8354  pwxpndom2  8434  adderpqlem  8725  addassnq  8729  mulcanenq  8731  distrnq  8732  ltanq  8742  ltexnq  8746  halfnq  8747  ltrnq  8750  archnq  8751  addclprlem2  8788  prlem934  8804  prlem936  8818  addcmpblnr  8841  mulcmpblnrlem  8842  ltsrpr  8846  m1p1sr  8861  m1m1sr  8862  0idsr  8866  1idsr  8867  00sr  8868  pn0sr  8870  recexsrlem  8872  mulgt0sr  8874  sqgt0sr  8875  mulresr  8908  axmulcom  8924  axmulass  8926  axdistr  8927  axi2m1  8928  ax1rid  8930  axcnre  8933  mul02lem1  9135  addid1  9139  add42i  9179  negid  9241  negsub  9242  subneg  9243  negsubdii  9278  muleqadd  9559  crne0  9886  2p2e4  9991  3p2e5  10004  3p3e6  10005  4p2e6  10006  4p3e7  10007  4p4e8  10008  5p2e7  10009  5p3e8  10010  5p4e9  10011  5p5e10  10012  6p2e8  10013  6p3e9  10014  6p4e10  10015  7p2e9  10016  7p3e10  10017  8p2e10  10018  3t3e9  10022  8th4div3  10084  halfpm6th  10085  addltmul  10096  nn0n0n1ge2  10173  nneo  10246  zeo  10248  numsuc  10287  numltc  10295  numsucc  10301  numma  10306  nummul1c  10311  6p5lem  10324  4t3lem  10346  decbin2  10379  xmulmnf1  10748  fztp  10994  fzprval  10997  fztpval  10998  fzshftral  11024  fzo01  11070  fzo0to2pr  11071  fzo0to3tp  11072  fzo0to42pr  11073  quoremz  11123  quoremnn0ALT  11125  intfrac2  11126  intfracq  11127  sqval  11328  sqrecii  11351  cu2  11366  i3  11369  i4  11370  binom2i  11377  binom3  11387  crreczi  11391  nn0opthlem1  11448  facp1  11458  faclbnd  11468  faclbnd2  11469  faclbnd4lem1  11471  faclbnd4lem4  11474  bcn1  11491  bcn2  11497  hashgadd  11538  hashxplem  11583  hashmap  11585  hashfun  11587  hashbclem  11588  fz1isolem  11597  ccatlid  11635  ccatrid  11636  eqs1  11648  wrdeqs1cat  11676  cats1un  11677  cats1fvn  11709  cats1cat  11712  swrds2  11767  reim0  11810  cji  11851  sqrm1  11968  absi  11978  rddif  12031  iseraltlem2  12363  iseralt  12365  fsump1i  12440  fsummulc2  12454  incexclem  12503  incexc  12504  arisum2  12527  geoihalfsum  12546  mertenslem1  12548  mertens  12550  ef0lem  12568  ege2le3  12579  eft0val  12600  ef4p  12601  efgt1p2  12602  efgt1p  12603  tanval2  12621  efival  12640  ef01bndlem  12672  sin01bnd  12673  cos01bnd  12674  cos1bnd  12675  cos2bnd  12676  rpnnen2lem11  12711  sqr2irrlem  12734  odd2np1lem  12794  odd2np1  12795  oddp1even  12797  divalglem5  12804  divalglem6  12805  bits0  12827  0bits  12838  bitsinv1lem  12840  gcdaddmlem  12915  3prm  12983  phiprm  13053  eulerthlem2  13058  prmdiv  13061  opoe  13072  pythagtriplem12  13087  pythagtriplem14  13089  pcmpt  13148  pcfac  13155  prmpwdvds  13159  pockthi  13162  prmreclem2  13172  prmreclem6  13176  4sqlem5  13197  4sqlem13  13212  modxai  13291  mod2xnegi  13294  gcdi  13296  decexp2  13298  numexpp1  13301  numexp2x  13302  decsplit0b  13303  decsplit1  13305  decsplit  13306  2exp6  13309  2exp16  13311  prmlem0  13315  139prm  13333  163prm  13334  317prm  13335  631prm  13336  1259lem1  13337  1259lem3  13339  1259lem4  13340  1259lem5  13341  1259prm  13342  2503lem1  13343  2503lem2  13344  2503lem3  13345  2503prm  13346  4001lem1  13347  4001lem2  13348  4001lem3  13349  4001lem4  13350  ressinbas  13412  rescfth  14021  xpccatid  14172  oduval  14444  oppgmnd  15037  lsmmod2  15195  efgi0  15239  efgi1  15240  efginvrel2  15246  efgsval2  15252  efgsp1  15256  efgredleme  15262  efgredlemc  15264  efgcpbllemb  15274  frgpnabllem1  15371  lt6abl  15391  gsumsn  15430  gsum2d  15433  pwsgsum  15440  dprd0  15476  dprdf1  15478  dprd2da  15487  ablfac1lem  15513  pgpfac1lem3  15522  pgpfaclem1  15526  opprrng  15623  mulgass3  15629  ply1assa  16488  ply1coe  16578  zlmval  16687  znbas  16714  znzrh2  16716  restin  17114  imacmp  17341  concompcon  17375  uptx  17536  cnpflf2  17908  tmdgsum2  17992  tsmsres  18039  tsmsf1o  18040  tsmsmhm  18041  prdsxmet  18146  resspwsds  18149  prdsxmslem2  18288  metdcn2  18558  metdcn  18559  metdscn2  18575  iimulcn  18651  icchmeo  18654  xrhmeo  18659  cnrehmeo  18666  cnheiborlem  18667  evth  18672  evth2  18673  lebnumlem2  18675  reparphti  18710  pcoass  18737  pi1xfrcnv  18770  ipcau2  18879  minveclem4  19011  pjthlem1  19016  ovolunlem1a  19070  unmbl  19110  uniioombl  19159  iblitg  19338  dfitg  19339  itg0  19349  iblcnlem1  19357  itgcnlem  19359  itgabs  19404  limcdif  19441  limccnp  19456  limccnp2  19457  dvexp  19517  dvmptid  19521  dvmptc  19522  dvmptfsum  19537  dveflem  19541  dvsincos  19543  mvth  19554  dvlipcn  19556  dvivthlem1  19570  dvfsumle  19583  dvfsumlem2  19589  itgsubst  19611  evlsval  19618  mpff  19640  tdeglem4  19661  tdeglem2  19662  plypf1  19809  plymullem1  19811  coesub  19853  dgrmulc  19867  fta1lem  19902  vieta1lem1  19905  vieta1lem2  19906  aalioulem4  19930  aaliou3lem3  19939  abelthlem2  20026  abelthlem8  20033  abelthlem9  20034  sinhalfpilem  20052  efhalfpi  20057  cospi  20058  efipi  20059  sin2pi  20061  cos2pi  20062  ef2pi  20063  sin2pim  20071  cos2pim  20072  sinmpi  20073  cosmpi  20074  sinppi  20075  cosppi  20076  sincosq4sgn  20087  tangtx  20091  sincos4thpi  20099  sincos6thpi  20101  sincos3rdpi  20102  pige3  20103  abssinper  20104  efif1olem4  20125  efifo  20127  eff1o  20129  logneg  20160  logimul  20187  logneg2  20188  dvrelog  20206  logcnlem4  20214  dvlog  20220  dvlog2  20222  logtayl  20229  1cxp  20241  ecxp  20242  cxpsqr  20272  dvsqr  20306  root1eq1  20317  cxpeq  20319  ang180lem1  20329  ang180lem2  20330  1cubrlem  20359  1cubr  20360  dcubic2  20362  mcubic  20365  cubic2  20366  binom4  20368  dquartlem1  20369  dquartlem2  20370  dquart  20371  quart1lem  20373  quart1  20374  quartlem1  20375  asinsin  20410  asin1  20412  acos1  20413  atanlogsublem  20433  atanlogsub  20434  efiatan2  20435  2efiatan  20436  tanatan  20437  atanbnd  20444  atan1  20446  dvatan  20453  atantayl2  20456  leibpilem2  20459  leibpi  20460  log2cnv  20462  log2tlbnd  20463  log2ublem1  20464  log2ublem2  20465  log2ublem3  20466  log2ub  20467  birthday  20471  amgmlem  20506  emcllem5  20516  wilthlem2  20530  ftalem6  20538  basellem2  20542  basellem3  20543  basellem5  20545  basellem8  20548  cht1  20626  chp1  20628  1sgmprm  20661  ppiublem2  20665  ppiub  20666  chtublem  20673  chtub  20674  logfacbnd3  20685  bcp1ctr  20741  bclbnd  20742  bposlem1  20746  bposlem4  20749  bposlem6  20751  bposlem8  20753  bposlem9  20754  lgslem1  20758  lgsdir2lem1  20785  lgsdir2lem2  20786  lgsdir2lem3  20787  lgsdir2lem5  20789  lgs1  20800  lgseisenlem1  20811  lgseisenlem3  20813  lgsquadlem1  20816  lgsquadlem2  20817  lgsquad2lem2  20821  m1lgs  20824  2sqlem8  20834  2sqblem  20839  logdivsum  20905  mulog2sumlem2  20907  log2sumbnd  20916  selberglem1  20917  selberglem2  20918  pntrmax  20936  pntibndlem2  20963  pntibndlem3  20964  pntlemg  20970  pntlemr  20974  pntlemo  20979  ostth2lem3  21007  ostth2lem4  21008  smcnlem  21583  ipidsq  21599  dipcj  21603  dip0r  21606  nmlnoubi  21687  nmblolbii  21690  blocnilem  21695  ip1ilem  21717  ip2i  21719  ipdirilem  21720  ipasslem10  21730  ipasslem11  21731  siilem1  21742  hvmul0  21916  hvsubsub4i  21951  hvnegdii  21954  hvsubeq0i  21955  hvsubcan2i  21956  hvsubaddi  21958  hvsub0  21968  hisubcomi  21996  normlem0  22001  normlem1  22002  normlem2  22003  normlem3  22004  normlem9  22010  norm-ii-i  22029  norm3difi  22039  normpari  22046  polid2i  22049  polidi  22050  bcsiALT  22071  pjhthlem1  22283  chdmm3i  22371  chdmm4i  22372  chjidm  22412  chj4i  22415  chjjdiri  22416  spanunsni  22471  pjoml4i  22479  cmcm2i  22485  qlax4i  22522  qlax5i  22523  pjadjii  22566  pjmulii  22569  pjsubii  22570  pjssmii  22573  pjcji  22576  pjneli  22615  hoadd32i  22671  ho0subi  22688  hosubid1  22691  hosd2i  22716  hopncani  22717  hosubeq0i  22719  lnopeq0lem1  22898  lnopunilem1  22903  lnophmlem2  22910  nmbdoplbi  22917  nmcopexi  22920  lnfnmuli  22937  nmcfnexi  22944  nmoptri2i  22992  nmopcoadji  22994  golem1  23164  mdsl1i  23214  cvmdi  23217  mdslmd3i  23225  csmdsymi  23227  xrge00  23599  gsumconstf  23613  raddcn  23670  xrge0iifhom  23678  xrge0mulc1cn  23682  cbvesum  23903  gsumesum  23916  esumpfinvallem  23929  esumpfinvalf  23931  dya2icoseg  24090  orrvcval4  24170  orrvcoel  24171  orrvccel  24172  coinflipprob  24185  coinflippvt  24190  ballotlem2  24194  ballotth  24243  lgamgulmlem2  24262  lgamgulmlem5  24265  lgam1  24296  subfacp1lem1  24313  subfacp1lem5  24318  subfacval2  24321  subfaclim  24322  subfacval3  24323  cvxpcon  24376  cvxscon  24377  vdgr1c  24483  vdegp1ai  24495  vdegp1bi  24496  vdegp1ci  24497  sinccvglem  24592  4bc3eq4  24687  4bc2eq6  24688  risefall0lem  24814  risefac1  24819  fallfac1  24820  faclimlem1  24837  frrlem5  25026  ax5seglem7  25305  axlowdimlem4  25315  axlowdimlem16  25327  bpoly0  25527  bpoly1  25528  bpolydiflem  25531  bpoly2  25534  bpoly3  25535  bpoly4  25536  fsumcube  25537  itgaddnclem2  25682  itgabsnc  25692  dvreasin  25698  areacirclem2  25700  areacirclem5  25704  areacirc  25706  prdstotbnd  26024  prdsbnd2  26025  repwsmet  26064  rrnequiv  26065  reheibor  26069  mapfzcons  26299  mapfzcons1cl  26301  2rexfrabdioph  26383  3rexfrabdioph  26384  4rexfrabdioph  26385  6rexfrabdioph  26386  7rexfrabdioph  26387  rabdiophlem2  26389  diophren  26402  rabren3dioph  26404  pellexlem5  26424  pell1qr1  26462  rmspecfund  26500  jm2.17a  26553  jm2.17b  26554  jm2.27c  26606  jm2.27dlem5  26612  lmhmlnmsplit  26691  dsmmval2  26708  psgnunilem2  26924  psgnunilem4  26926  psgnpmtr  26939  lhe4.4ex1a  27052  expgrowthi  27056  expgrowth  27058  refsumcn  27207  m1expeven  27231  dvcosre  27247  itgsin0pilem1  27250  itgsinexplem1  27254  stoweidlem13  27268  wallispilem4  27323  wallispi2lem1  27326  wallispi2lem2  27327  stirlinglem1  27329  0wlk  27699  0trl  27700  wlkntrllem3  27705  wlkntrllem4  27706  constr1trl  27726  1pthonlem1  27727  2trllem3  27734  constr2trl  27736  wlkdvspthlem  27745  usgrcyclnl2  27767  constr3trllem3  27778  constr3trllem4  27779  constr3trllem5  27780  constr3pthlem1  27781  constr3pthlem3  27783  vdgre1c  27814  sec0  27932  elogb  27961  dalem-cly  29931  pmodN  30110  cdleme0cp  30474  cdleme0cq  30475  cdleme1  30487  cdleme3d  30491  cdleme3h  30495  cdleme4  30498  cdleme5  30500  cdleme7a  30503  cdleme8  30510  cdleme9  30513  cdleme10  30514  cdleme11g  30525  cdleme15b  30535  cdleme21  30597  cdleme22e  30604  cdleme22eALTN  30605  cdleme23c  30611  cdleme25cv  30618  cdleme35b  30710  cdleme35c  30711  cdleme42a  30731  cdleme42d  30733  cdleme43aN  30749  cdlemeg46gfv  30790  cdlemk35  31172  dihjatcclem1  31679  lcdval2  31851  mapdpglem21  31953
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1551  ax-5 1562  ax-17 1621  ax-9 1659  ax-8 1680  ax-6 1734  ax-7 1739  ax-11 1751  ax-12 1937  ax-ext 2347
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 937  df-tru 1324  df-ex 1547  df-nf 1550  df-sb 1654  df-clab 2353  df-cleq 2359  df-clel 2362  df-nfc 2491  df-rex 2634  df-rab 2637  df-v 2875  df-dif 3241  df-un 3243  df-in 3245  df-ss 3252  df-nul 3544  df-if 3655  df-sn 3735  df-pr 3736  df-op 3738  df-uni 3930  df-br 4126  df-iota 5322  df-fv 5366  df-ov 5984
  Copyright terms: Public domain W3C validator