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

Theorem oveq2i 6201
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 6198 . 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 1370  (class class class)co 6190
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-rex 2801  df-rab 2804  df-v 3070  df-dif 3429  df-un 3431  df-in 3433  df-ss 3440  df-nul 3736  df-if 3890  df-sn 3976  df-pr 3978  df-op 3982  df-uni 4190  df-br 4391  df-iota 5479  df-fv 5524  df-ov 6193
This theorem is referenced by:  caov32  6390  caov4  6394  caov42  6396  seqomsuc  7012  oa1suc  7071  om1  7081  oe1  7083  oawordeulem  7093  oeoalem  7135  nnm1  7187  nnm2  7188  nneob  7191  omopthlem1  7194  mapsnconst  7358  mapsncnv  7359  map2xp  7581  cantnflt  7981  cantnfltOLD  8011  cnfcom2  8036  cnfcom2OLD  8044  infxpenc  8285  infxpenc2  8289  infxpencOLD  8290  infxpenc2OLD  8293  ackbij1lem5  8494  alephom  8850  pwxpndom2  8933  adderpqlem  9224  addassnq  9228  mulcanenq  9230  distrnq  9231  ltanq  9241  ltexnq  9245  halfnq  9246  ltrnq  9249  archnq  9250  addclprlem2  9287  prlem934  9303  prlem936  9317  addcmpblnr  9340  mulcmpblnrlem  9341  ltsrpr  9345  m1p1sr  9360  m1m1sr  9361  0idsr  9365  1idsr  9366  00sr  9367  pn0sr  9369  recexsrlem  9371  mulgt0sr  9373  sqgt0sr  9374  mulresr  9407  axmulcom  9423  axmulass  9425  axdistr  9426  axi2m1  9427  ax1rid  9429  axcnre  9432  mul02lem1  9646  addid1  9650  add42i  9691  negid  9757  negsub  9758  subneg  9759  negsubdii  9794  muleqadd  10081  crne0  10416  2p2e4  10540  3p2e5  10555  3p3e6  10556  4p2e6  10557  4p3e7  10558  4p4e8  10559  5p2e7  10560  5p3e8  10561  5p4e9  10562  5p5e10  10563  6p2e8  10564  6p3e9  10565  6p4e10  10566  7p2e9  10567  7p3e10  10568  8p2e10  10569  3t3e9  10575  8th4div3  10646  halfpm6th  10647  addltmul  10661  nn0n0n1ge2  10744  nneo  10826  zeo  10828  numsuc  10868  numltc  10876  numsucc  10882  numma  10887  nummul1c  10892  6p5lem  10905  4t3lem  10927  decbin2  10960  xmulmnf1  11340  fztp  11613  fz0tp  11614  fzprval  11618  fztpval  11619  fzshftral  11648  fzo01  11713  fzo12sn  11714  fzo0to2pr  11715  fzo0to3tp  11716  fzo0to42pr  11717  quoremz  11795  quoremnn0ALT  11797  intfrac2  11798  intfracq  11799  sqval  12026  sqrecii  12049  cu2  12065  i3  12068  i4  12069  binom2i  12076  binom3  12086  crreczi  12090  nn0opthlem1  12147  facp1  12157  faclbnd  12167  faclbnd2  12168  faclbnd4lem1  12170  faclbnd4lem4  12173  bcn1  12190  bcn2  12196  hashgadd  12242  hashxplem  12297  hashmap  12299  hashfun  12301  hashbclem  12307  fz1isolem  12316  ccatlid  12386  ccatrid  12387  eqs1  12402  ccats1val2  12409  wrdeqs1cat  12471  cats1un  12472  swrdccatin12lem3  12483  swrdccat3a  12487  cats1fvn  12587  cats1cat  12590  swrds2  12647  reim0  12709  cji  12750  sqrm1  12867  absi  12877  rddif  12930  iseraltlem2  13262  iseralt  13264  fsump1i  13338  fsummulc2  13353  incexclem  13401  incexc  13402  arisum2  13425  geoihalfsum  13444  mertenslem1  13446  mertens  13448  ef0lem  13466  ege2le3  13477  eft0val  13498  ef4p  13499  efgt1p2  13500  efgt1p  13501  tanval2  13519  efival  13538  ef01bndlem  13570  sin01bnd  13571  cos01bnd  13572  cos1bnd  13573  cos2bnd  13574  rpnnen2lem11  13609  sqr2irrlem  13632  odd2np1lem  13693  odd2np1  13694  oddp1even  13696  divalglem5  13703  divalglem6  13704  bits0  13726  0bits  13737  gcdaddmlem  13814  3prm  13882  phiprm  13954  eulerthlem2  13959  prmdiv  13962  opoe  13980  pythagtriplem12  13995  pythagtriplem14  13997  pcmpt  14056  pcfac  14063  prmpwdvds  14067  pockthi  14070  prmreclem2  14080  prmreclem6  14084  4sqlem5  14105  4sqlem13  14120  modxai  14199  mod2xnegi  14202  gcdi  14204  decexp2  14206  numexpp1  14209  numexp2x  14210  decsplit0b  14211  decsplit1  14213  decsplit  14214  2exp6  14217  2exp16  14219  prmlem0  14235  139prm  14253  163prm  14254  317prm  14255  631prm  14256  1259lem1  14257  1259lem3  14259  1259lem4  14260  1259lem5  14261  1259prm  14262  2503lem1  14263  2503lem2  14264  2503lem3  14265  2503prm  14266  4001lem1  14267  4001lem2  14268  4001lem3  14269  4001lem4  14270  ressinbas  14336  rescfth  14949  xpccatid  15100  oduval  15402  oppgmnd  15971  psgnunilem2  16103  psgnunilem4  16105  psgnpmtr  16118  psgn0fv0  16119  psgnsn  16128  psgnprfval1  16130  lsmmod2  16277  efgi0  16321  efgi1  16322  efginvrel2  16328  efgsval2  16334  efgsp1  16338  efgredleme  16344  efgredlemc  16346  efgcpbllemb  16356  frgpnabllem1  16455  lt6abl  16475  gsumconstf  16533  gsumsn  16554  gsum2dlem2  16567  gsum2dOLD  16569  pwsgsum  16578  pwsgsumOLD  16579  dprd0  16633  dprdf1  16635  dprd2da  16646  ablfac1lem  16674  pgpfac1lem3  16683  pgpfaclem1  16687  srgbinomlem4  16747  opprrng  16829  mulgass3  16835  evlsval  17712  mpff  17726  ply1assa  17762  gsumply1subr  17795  ply1coe  17855  ply1coeOLD  17856  evl1gsumdlem  17899  evl1gsumd  17900  znbas  18085  znzrh2  18087  dsmmval2  18270  frlmip  18312  madetsumid  18457  mdetrsca  18525  mdetrsca2  18526  mdettpos  18533  m2detleiblem2  18550  madugsum  18565  madurid  18566  restin  18886  imacmp  19116  concompcon  19152  uptx  19314  cnpflf2  19689  tmdgsum2  19783  tsmsresOLD  19833  tsmsres  19834  tsmsf1o  19835  tsmsmhm  19836  prdsxmet  20060  resspwsds  20063  prdsxmslem2  20220  metdcn2  20532  metdcn  20533  metdscn2  20549  iimulcn  20626  icchmeo  20629  xrhmeo  20634  cnrehmeo  20641  cnheiborlem  20642  evth  20647  evth2  20648  lebnumlem2  20650  reparphti  20685  pcoass  20712  pi1xfrcnv  20745  ipcau2  20865  minveclem4  21035  pjthlem1  21040  ovolunlem1a  21095  unmbl  21135  uniioombl  21185  iblitg  21362  dfitg  21363  itg0  21373  iblcnlem1  21381  itgcnlem  21383  itgabs  21428  limcdif  21467  limccnp  21482  limccnp2  21483  dvexp  21543  dvmptid  21547  dvmptc  21548  dvmptfsum  21563  dveflem  21567  dvsincos  21569  mvth  21580  dvlipcn  21582  dvivthlem1  21596  dvfsumle  21609  dvfsumlem2  21615  itgsubst  21637  tdeglem4  21645  tdeglem2  21646  plypf1  21796  plymullem1  21798  coesub  21840  dgrmulc  21854  fta1lem  21889  vieta1lem1  21892  vieta1lem2  21893  aalioulem4  21917  aaliou3lem3  21926  abelthlem2  22013  abelthlem8  22020  abelthlem9  22021  sinhalfpilem  22041  efhalfpi  22049  cospi  22050  efipi  22051  sin2pi  22053  cos2pi  22054  ef2pi  22055  sin2pim  22063  cos2pim  22064  sinmpi  22065  cosmpi  22066  sinppi  22067  cosppi  22068  sincosq4sgn  22079  tangtx  22083  sincos4thpi  22091  sincos6thpi  22093  sincos3rdpi  22094  pige3  22095  abssinper  22096  efif1olem4  22117  efifo  22119  eff1o  22121  logneg  22152  logimul  22179  logneg2  22180  dvrelog  22198  logcnlem4  22206  dvlog  22212  dvlog2  22214  logtayl  22221  1cxp  22233  ecxp  22234  cxpsqr  22264  dvsqr  22298  root1eq1  22309  cxpeq  22311  ang180lem1  22321  ang180lem2  22322  heron  22349  1cubrlem  22352  1cubr  22353  dcubic2  22355  mcubic  22358  cubic2  22359  binom4  22361  dquartlem1  22362  dquartlem2  22363  dquart  22364  quart1lem  22366  quart1  22367  quartlem1  22368  asinsin  22403  asin1  22405  acos1  22406  atanlogsublem  22426  atanlogsub  22427  efiatan2  22428  2efiatan  22429  tanatan  22430  atanbnd  22437  atan1  22439  dvatan  22446  atantayl2  22449  leibpilem2  22452  leibpi  22453  log2cnv  22455  log2tlbnd  22456  log2ublem1  22457  log2ublem2  22458  log2ublem3  22459  log2ub  22460  birthday  22464  amgmlem  22499  emcllem5  22509  wilthlem2  22523  ftalem6  22531  basellem2  22535  basellem3  22536  basellem5  22538  basellem8  22541  cht1  22619  chp1  22621  1sgmprm  22654  ppiublem2  22658  ppiub  22659  chtublem  22666  chtub  22667  logfacbnd3  22678  bcp1ctr  22734  bclbnd  22735  bposlem1  22739  bposlem4  22742  bposlem6  22744  bposlem8  22746  bposlem9  22747  lgslem1  22751  lgsdir2lem1  22778  lgsdir2lem2  22779  lgsdir2lem3  22780  lgsdir2lem5  22782  lgs1  22793  lgseisenlem1  22804  lgseisenlem3  22806  lgsquadlem1  22809  lgsquadlem2  22810  lgsquad2lem2  22814  m1lgs  22817  2sqlem8  22827  2sqblem  22832  logdivsum  22898  mulog2sumlem2  22900  log2sumbnd  22909  selberglem1  22910  selberglem2  22911  pntrmax  22929  pntibndlem2  22956  pntibndlem3  22957  pntlemg  22963  pntlemr  22967  pntlemo  22972  ostth2lem3  23000  ostth2lem4  23001  trgcgrg  23086  colperplem1  23240  ax5seglem7  23316  axlowdimlem4  23326  axlowdimlem16  23338  0wlk  23579  0trl  23580  wlkntrllem2  23594  wlkntrl  23596  constr1trl  23622  1pthonlem1  23623  constr2wlk  23632  constr2trl  23633  wlkdvspthlem  23641  constr3trllem3  23673  constr3trllem4  23674  constr3trllem5  23675  constr3pthlem1  23676  constr3pthlem3  23678  vdgr1c  23710  vdegp1ai  23740  vdegp1bi  23741  vdegp1ci  23742  smcnlem  24227  ipidsq  24243  dipcj  24247  dip0r  24250  nmlnoubi  24331  nmblolbii  24334  blocnilem  24339  ip1ilem  24361  ip2i  24363  ipdirilem  24364  ipasslem10  24374  ipasslem11  24375  siilem1  24386  hvmul0  24561  hvsubsub4i  24596  hvnegdii  24599  hvsubeq0i  24600  hvsubcan2i  24601  hvsubaddi  24603  hvsub0  24613  hisubcomi  24641  normlem0  24646  normlem1  24647  normlem2  24648  normlem3  24649  normlem9  24655  norm-ii-i  24674  norm3difi  24684  normpari  24691  polid2i  24694  polidi  24695  bcsiALT  24716  pjhthlem1  24929  chdmm3i  25017  chdmm4i  25018  chjidm  25058  chj4i  25061  chjjdiri  25062  spanunsni  25117  pjoml4i  25125  cmcm2i  25131  qlax4i  25168  qlax5i  25169  pjadjii  25212  pjmulii  25215  pjsubii  25216  pjssmii  25219  pjcji  25222  pjneli  25261  hoadd32i  25317  ho0subi  25334  hosubid1  25337  hosd2i  25362  hopncani  25363  hosubeq0i  25365  lnopeq0lem1  25544  lnopunilem1  25549  lnophmlem2  25556  nmbdoplbi  25563  nmcopexi  25566  lnfnmuli  25583  nmcfnexi  25590  nmoptri2i  25638  nmopcoadji  25640  golem1  25810  mdsl1i  25860  cvmdi  25863  mdslmd3i  25871  csmdsymi  25873  xrge00  26281  archirngz  26340  archiabllem2c  26346  gsumsnf  26378  gsumle  26380  gsummptun  26382  gsumvsca1  26385  gsumvsca2  26386  xrge0slmod  26446  raddcn  26493  xrge0iifhom  26501  xrge0mulc1cn  26505  cbvesum  26631  gsumesum  26644  esumpfinvallem  26657  esumpfinvalf  26659  dya2icoseg  26826  sitg0  26866  eulerpartlemd  26883  eulerpartlemgvv  26893  eulerpartlemgh  26895  fib0  26916  fib1  26917  fibp1  26918  orrvcval4  26981  orrvcoel  26982  orrvccel  26983  coinflipprob  26996  coinflippvt  27001  ballotlem2  27005  ballotth  27054  signstf0  27103  signstfvn  27104  signsvtn0  27105  signstfvp  27106  signstfvneq0  27107  signstfveq0  27112  signsvf0  27115  signsvf1  27116  signsvfn  27117  signshf  27123  lgamgulmlem2  27150  lgamgulmlem5  27153  lgam1  27184  subfacp1lem1  27201  subfacp1lem5  27206  subfacval2  27209  subfaclim  27210  subfacval3  27211  cvxpcon  27265  cvxscon  27266  problem4  27435  quad3  27437  sinccvglem  27451  4bc3eq4  27524  4bc2eq6  27525  risefall0lem  27663  risefac1  27670  fallfac1  27671  fallfacfwd  27673  faclimlem1  27683  frrlem5  27906  bpoly0  28327  bpoly1  28328  bpolydiflem  28331  bpoly2  28334  bpoly3  28335  bpoly4  28336  fsumcube  28337  ptrest  28563  dvtan  28580  itgabsnc  28599  ftc1anclem8  28612  dvcnsqr  28616  dvasin  28618  dvacos  28619  areacirclem1  28622  areacirclem4  28625  areacirc  28627  prdstotbnd  28831  prdsbnd2  28832  repwsmet  28871  rrnequiv  28872  reheibor  28876  mapfzcons  29190  mapfzcons1cl  29192  2rexfrabdioph  29272  3rexfrabdioph  29273  4rexfrabdioph  29274  6rexfrabdioph  29275  7rexfrabdioph  29276  rabdiophlem2  29278  diophren  29290  rabren3dioph  29292  pellexlem5  29312  pell1qr1  29350  rmspecfund  29388  jm2.17a  29441  jm2.17b  29442  jm2.27c  29494  jm2.27dlem5  29500  lmhmlnmsplit  29578  arearect  29729  areaquad  29730  lhe4.4ex1a  29741  expgrowthi  29745  expgrowth  29747  refsumcn  29890  m1expeven  29910  dvcosre  29926  itgsin0pilem1  29928  itgsinexplem1  29932  stoweidlem13  29946  wallispilem4  30001  wallispi2lem1  30004  wallispi2lem2  30005  stirlinglem1  30007  f13idfv  30286  ccat2s1p2  30404  ccatw2s1p2  30408  clwwlkn2  30576  clwlkisclwwlk2  30590  wwlkext2clwwlk  30603  nbhashuvtx1  30671  extwwlkfablem2  30809  numclwwlkovf2ex  30817  numclwlk2lem2f  30834  frgraregord013  30849  2t6m3t4e0  30878  fsfnn0gsumfsffz  30944  coe1fzgsumdlem  30979  coe1fzgsumd  30980  gsumply1eq  30994  matgsum  31015  zlmodzxzequa  31145  zlmodzxznm  31146  zlmodzxzequap  31148  cpmat  31172  pmatcollpw3fi  31239  pmatcollpw4fi1lem1  31242  mp2pm2mplem5  31265  pmattomply1fo  31268  pmattomply1mhmlem2  31274  cpmat1dlem  31289  cpmat1d  31290  cpidmat  31301  cpmidpmat  31327  cpmadugsumfi  31331  chcoeffeqlem  31340  cayleyhamilton0  31344  cayleyhamiltonALT  31346  cayleyhamilton1  31347  sec0  31391  elogb  31406  dalem-cly  33621  pmodN  33800  cdleme0cp  34164  cdleme0cq  34165  cdleme1  34177  cdleme3d  34181  cdleme3h  34185  cdleme4  34188  cdleme5  34190  cdleme7a  34193  cdleme8  34200  cdleme9  34203  cdleme10  34204  cdleme11g  34215  cdleme15b  34225  cdleme21  34287  cdleme22e  34294  cdleme22eALTN  34295  cdleme23c  34301  cdleme25cv  34308  cdleme35b  34400  cdleme35c  34401  cdleme42a  34421  cdleme42d  34423  cdleme43aN  34439  cdlemeg46gfv  34480  cdlemk35  34862  dihjatcclem1  35369  lcdval2  35541  mapdpglem21  35643
  Copyright terms: Public domain W3C validator