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

Theorem oveq2i 6091
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 6088 . 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 1362  (class class class)co 6080
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 960  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-rex 2711  df-rab 2714  df-v 2964  df-dif 3319  df-un 3321  df-in 3323  df-ss 3330  df-nul 3626  df-if 3780  df-sn 3866  df-pr 3868  df-op 3872  df-uni 4080  df-br 4281  df-iota 5369  df-fv 5414  df-ov 6083
This theorem is referenced by:  caov32  6279  caov4  6283  caov42  6285  seqomsuc  6898  oa1suc  6959  om1  6969  oe1  6971  oawordeulem  6981  oeoalem  7023  nnm1  7075  nnm2  7076  nneob  7079  omopthlem1  7082  mapsnconst  7246  mapsncnv  7247  map2xp  7469  cantnflt  7868  cantnfltOLD  7898  cnfcom2  7923  cnfcom2OLD  7931  infxpenc  8172  infxpenc2  8176  infxpencOLD  8177  infxpenc2OLD  8180  ackbij1lem5  8381  alephom  8737  pwxpndom2  8820  adderpqlem  9111  addassnq  9115  mulcanenq  9117  distrnq  9118  ltanq  9128  ltexnq  9132  halfnq  9133  ltrnq  9136  archnq  9137  addclprlem2  9174  prlem934  9190  prlem936  9204  addcmpblnr  9227  mulcmpblnrlem  9228  ltsrpr  9232  m1p1sr  9247  m1m1sr  9248  0idsr  9252  1idsr  9253  00sr  9254  pn0sr  9256  recexsrlem  9258  mulgt0sr  9260  sqgt0sr  9261  mulresr  9294  axmulcom  9310  axmulass  9312  axdistr  9313  axi2m1  9314  ax1rid  9316  axcnre  9319  mul02lem1  9533  addid1  9537  add42i  9578  negid  9644  negsub  9645  subneg  9646  negsubdii  9681  muleqadd  9968  crne0  10303  2p2e4  10427  3p2e5  10442  3p3e6  10443  4p2e6  10444  4p3e7  10445  4p4e8  10446  5p2e7  10447  5p3e8  10448  5p4e9  10449  5p5e10  10450  6p2e8  10451  6p3e9  10452  6p4e10  10453  7p2e9  10454  7p3e10  10455  8p2e10  10456  3t3e9  10462  8th4div3  10533  halfpm6th  10534  addltmul  10548  nn0n0n1ge2  10631  nneo  10713  zeo  10715  numsuc  10755  numltc  10763  numsucc  10769  numma  10774  nummul1c  10779  6p5lem  10792  4t3lem  10814  decbin2  10847  xmulmnf1  11227  fztp  11497  fz0tp  11498  fzprval  11501  fztpval  11502  fzshftral  11531  fzo01  11596  fzo12sn  11597  fzo0to2pr  11598  fzo0to3tp  11599  fzo0to42pr  11600  quoremz  11678  quoremnn0ALT  11680  intfrac2  11681  intfracq  11682  sqval  11909  sqrecii  11932  cu2  11948  i3  11951  i4  11952  binom2i  11959  binom3  11969  crreczi  11973  nn0opthlem1  12030  facp1  12040  faclbnd  12050  faclbnd2  12051  faclbnd4lem1  12053  faclbnd4lem4  12056  bcn1  12073  bcn2  12079  hashgadd  12124  hashxplem  12179  hashmap  12181  hashfun  12183  hashbclem  12189  fz1isolem  12198  ccatlid  12268  ccatrid  12269  eqs1  12284  ccats1val2  12291  wrdeqs1cat  12353  cats1un  12354  swrdccatin12lem3  12365  swrdccat3a  12369  cats1fvn  12469  cats1cat  12472  swrds2  12529  reim0  12591  cji  12632  sqrm1  12749  absi  12759  rddif  12812  iseraltlem2  13144  iseralt  13146  fsump1i  13220  fsummulc2  13234  incexclem  13282  incexc  13283  arisum2  13306  geoihalfsum  13325  mertenslem1  13327  mertens  13329  ef0lem  13347  ege2le3  13358  eft0val  13379  ef4p  13380  efgt1p2  13381  efgt1p  13382  tanval2  13400  efival  13419  ef01bndlem  13451  sin01bnd  13452  cos01bnd  13453  cos1bnd  13454  cos2bnd  13455  rpnnen2lem11  13490  sqr2irrlem  13513  odd2np1lem  13574  odd2np1  13575  oddp1even  13577  divalglem5  13584  divalglem6  13585  bits0  13607  0bits  13618  gcdaddmlem  13695  3prm  13763  phiprm  13835  eulerthlem2  13840  prmdiv  13843  opoe  13861  pythagtriplem12  13876  pythagtriplem14  13878  pcmpt  13937  pcfac  13944  prmpwdvds  13948  pockthi  13951  prmreclem2  13961  prmreclem6  13965  4sqlem5  13986  4sqlem13  14001  modxai  14080  mod2xnegi  14083  gcdi  14085  decexp2  14087  numexpp1  14090  numexp2x  14091  decsplit0b  14092  decsplit1  14094  decsplit  14095  2exp6  14098  2exp16  14100  prmlem0  14116  139prm  14134  163prm  14135  317prm  14136  631prm  14137  1259lem1  14138  1259lem3  14140  1259lem4  14141  1259lem5  14142  1259prm  14143  2503lem1  14144  2503lem2  14145  2503lem3  14146  2503prm  14147  4001lem1  14148  4001lem2  14149  4001lem3  14150  4001lem4  14151  ressinbas  14217  rescfth  14830  xpccatid  14981  oduval  15283  oppgmnd  15849  psgnunilem2  15981  psgnunilem4  15983  psgnpmtr  15996  psgn0fv0  15997  psgnprfval1  16006  lsmmod2  16153  efgi0  16197  efgi1  16198  efginvrel2  16204  efgsval2  16210  efgsp1  16214  efgredleme  16220  efgredlemc  16222  efgcpbllemb  16232  frgpnabllem1  16331  lt6abl  16351  gsumsn  16425  gsum2dlem2  16436  gsum2dOLD  16438  pwsgsum  16447  pwsgsumOLD  16448  dprd0  16502  dprdf1  16504  dprd2da  16515  ablfac1lem  16543  pgpfac1lem3  16552  pgpfaclem1  16556  opprrng  16657  mulgass3  16663  ply1assa  17554  ply1coe  17643  znbas  17818  znzrh2  17820  dsmmval2  18003  frlmip  18045  madetsumid  18188  mdetrsca  18252  mdetrsca2  18253  mdettpos  18259  m2detleiblem2  18276  madugsum  18291  madurid  18292  restin  18612  imacmp  18842  concompcon  18878  uptx  19040  cnpflf2  19415  tmdgsum2  19509  tsmsresOLD  19559  tsmsres  19560  tsmsf1o  19561  tsmsmhm  19562  prdsxmet  19786  resspwsds  19789  prdsxmslem2  19946  metdcn2  20258  metdcn  20259  metdscn2  20275  iimulcn  20352  icchmeo  20355  xrhmeo  20360  cnrehmeo  20367  cnheiborlem  20368  evth  20373  evth2  20374  lebnumlem2  20376  reparphti  20411  pcoass  20438  pi1xfrcnv  20471  ipcau2  20591  minveclem4  20761  pjthlem1  20766  ovolunlem1a  20821  unmbl  20861  uniioombl  20911  iblitg  21088  dfitg  21089  itg0  21099  iblcnlem1  21107  itgcnlem  21109  itgabs  21154  limcdif  21193  limccnp  21208  limccnp2  21209  dvexp  21269  dvmptid  21273  dvmptc  21274  dvmptfsum  21289  dveflem  21293  dvsincos  21295  mvth  21306  dvlipcn  21308  dvivthlem1  21322  dvfsumle  21335  dvfsumlem2  21341  itgsubst  21363  evlsval  21371  mpff  21393  tdeglem4  21414  tdeglem2  21415  plypf1  21565  plymullem1  21567  coesub  21609  dgrmulc  21623  fta1lem  21658  vieta1lem1  21661  vieta1lem2  21662  aalioulem4  21686  aaliou3lem3  21695  abelthlem2  21782  abelthlem8  21789  abelthlem9  21790  sinhalfpilem  21810  efhalfpi  21818  cospi  21819  efipi  21820  sin2pi  21822  cos2pi  21823  ef2pi  21824  sin2pim  21832  cos2pim  21833  sinmpi  21834  cosmpi  21835  sinppi  21836  cosppi  21837  sincosq4sgn  21848  tangtx  21852  sincos4thpi  21860  sincos6thpi  21862  sincos3rdpi  21863  pige3  21864  abssinper  21865  efif1olem4  21886  efifo  21888  eff1o  21890  logneg  21921  logimul  21948  logneg2  21949  dvrelog  21967  logcnlem4  21975  dvlog  21981  dvlog2  21983  logtayl  21990  1cxp  22002  ecxp  22003  cxpsqr  22033  dvsqr  22067  root1eq1  22078  cxpeq  22080  ang180lem1  22090  ang180lem2  22091  heron  22118  1cubrlem  22121  1cubr  22122  dcubic2  22124  mcubic  22127  cubic2  22128  binom4  22130  dquartlem1  22131  dquartlem2  22132  dquart  22133  quart1lem  22135  quart1  22136  quartlem1  22137  asinsin  22172  asin1  22174  acos1  22175  atanlogsublem  22195  atanlogsub  22196  efiatan2  22197  2efiatan  22198  tanatan  22199  atanbnd  22206  atan1  22208  dvatan  22215  atantayl2  22218  leibpilem2  22221  leibpi  22222  log2cnv  22224  log2tlbnd  22225  log2ublem1  22226  log2ublem2  22227  log2ublem3  22228  log2ub  22229  birthday  22233  amgmlem  22268  emcllem5  22278  wilthlem2  22292  ftalem6  22300  basellem2  22304  basellem3  22305  basellem5  22307  basellem8  22310  cht1  22388  chp1  22390  1sgmprm  22423  ppiublem2  22427  ppiub  22428  chtublem  22435  chtub  22436  logfacbnd3  22447  bcp1ctr  22503  bclbnd  22504  bposlem1  22508  bposlem4  22511  bposlem6  22513  bposlem8  22515  bposlem9  22516  lgslem1  22520  lgsdir2lem1  22547  lgsdir2lem2  22548  lgsdir2lem3  22549  lgsdir2lem5  22551  lgs1  22562  lgseisenlem1  22573  lgseisenlem3  22575  lgsquadlem1  22578  lgsquadlem2  22579  lgsquad2lem2  22583  m1lgs  22586  2sqlem8  22596  2sqblem  22601  logdivsum  22667  mulog2sumlem2  22669  log2sumbnd  22678  selberglem1  22679  selberglem2  22680  pntrmax  22698  pntibndlem2  22725  pntibndlem3  22726  pntlemg  22732  pntlemr  22736  pntlemo  22741  ostth2lem3  22769  ostth2lem4  22770  trgcgrg  22848  ax5seglem7  23004  axlowdimlem4  23014  axlowdimlem16  23026  0wlk  23267  0trl  23268  wlkntrllem2  23282  wlkntrl  23284  constr1trl  23310  1pthonlem1  23311  constr2wlk  23320  constr2trl  23321  wlkdvspthlem  23329  constr3trllem3  23361  constr3trllem4  23362  constr3trllem5  23363  constr3pthlem1  23364  constr3pthlem3  23366  vdgr1c  23398  vdegp1ai  23428  vdegp1bi  23429  vdegp1ci  23430  smcnlem  23915  ipidsq  23931  dipcj  23935  dip0r  23938  nmlnoubi  24019  nmblolbii  24022  blocnilem  24027  ip1ilem  24049  ip2i  24051  ipdirilem  24052  ipasslem10  24062  ipasslem11  24063  siilem1  24074  hvmul0  24249  hvsubsub4i  24284  hvnegdii  24287  hvsubeq0i  24288  hvsubcan2i  24289  hvsubaddi  24291  hvsub0  24301  hisubcomi  24329  normlem0  24334  normlem1  24335  normlem2  24336  normlem3  24337  normlem9  24343  norm-ii-i  24362  norm3difi  24372  normpari  24379  polid2i  24382  polidi  24383  bcsiALT  24404  pjhthlem1  24617  chdmm3i  24705  chdmm4i  24706  chjidm  24746  chj4i  24749  chjjdiri  24750  spanunsni  24805  pjoml4i  24813  cmcm2i  24819  qlax4i  24856  qlax5i  24857  pjadjii  24900  pjmulii  24903  pjsubii  24904  pjssmii  24907  pjcji  24910  pjneli  24949  hoadd32i  25005  ho0subi  25022  hosubid1  25025  hosd2i  25050  hopncani  25051  hosubeq0i  25053  lnopeq0lem1  25232  lnopunilem1  25237  lnophmlem2  25244  nmbdoplbi  25251  nmcopexi  25254  lnfnmuli  25271  nmcfnexi  25278  nmoptri2i  25326  nmopcoadji  25328  golem1  25498  mdsl1i  25548  cvmdi  25551  mdslmd3i  25559  csmdsymi  25561  xrge00  25970  archirngz  26030  archiabllem2c  26036  gsumconstf  26095  gsumsnf  26096  gsumle  26098  gsummptun  26100  gsumvsca1  26104  gsumvsca2  26105  xrge0slmod  26166  raddcn  26213  xrge0iifhom  26221  xrge0mulc1cn  26225  cbvesum  26351  gsumesum  26364  esumpfinvallem  26377  esumpfinvalf  26379  dya2icoseg  26546  sitg0  26580  eulerpartlemd  26597  eulerpartlemgvv  26607  eulerpartlemgh  26609  fib0  26630  fib1  26631  fibp1  26632  orrvcval4  26695  orrvcoel  26696  orrvccel  26697  coinflipprob  26710  coinflippvt  26715  ballotlem2  26719  ballotth  26768  signstf0  26817  signstfvn  26818  signsvtn0  26819  signstfvp  26820  signstfvneq0  26821  signstfveq0  26826  signsvf0  26829  signsvf1  26830  signsvfn  26831  signshf  26837  lgamgulmlem2  26864  lgamgulmlem5  26867  lgam1  26898  subfacp1lem1  26915  subfacp1lem5  26920  subfacval2  26923  subfaclim  26924  subfacval3  26925  cvxpcon  26979  cvxscon  26980  problem4  27149  sinccvglem  27164  4bc3eq4  27237  4bc2eq6  27238  risefall0lem  27376  risefac1  27383  fallfac1  27384  fallfacfwd  27386  faclimlem1  27396  frrlem5  27619  bpoly0  28040  bpoly1  28041  bpolydiflem  28044  bpoly2  28047  bpoly3  28048  bpoly4  28049  fsumcube  28050  ptrest  28269  dvtan  28286  itgabsnc  28305  ftc1anclem8  28318  dvcnsqr  28322  dvasin  28324  dvacos  28325  areacirclem1  28328  areacirclem4  28331  areacirc  28333  prdstotbnd  28537  prdsbnd2  28538  repwsmet  28577  rrnequiv  28578  reheibor  28582  mapfzcons  28897  mapfzcons1cl  28899  2rexfrabdioph  28979  3rexfrabdioph  28980  4rexfrabdioph  28981  6rexfrabdioph  28982  7rexfrabdioph  28983  rabdiophlem2  28985  diophren  28997  rabren3dioph  28999  pellexlem5  29019  pell1qr1  29057  rmspecfund  29095  jm2.17a  29148  jm2.17b  29149  jm2.27c  29201  jm2.27dlem5  29207  lmhmlnmsplit  29285  arearect  29436  areaquad  29437  lhe4.4ex1a  29448  expgrowthi  29452  expgrowth  29454  refsumcn  29597  m1expeven  29618  dvcosre  29634  itgsin0pilem1  29636  itgsinexplem1  29640  stoweidlem13  29654  wallispilem4  29709  wallispi2lem1  29712  wallispi2lem2  29713  stirlinglem1  29715  f13idfv  29994  ccat2s1p2  30112  ccatw2s1p2  30116  clwwlkn2  30284  clwlkisclwwlk2  30298  wwlkext2clwwlk  30311  nbhashuvtx1  30379  extwwlkfablem2  30517  numclwwlkovf2ex  30525  numclwlk2lem2f  30542  frgraregord013  30557  2t6m3t4e0  30584  psgnsn  30602  zlmodzxzequa  30747  zlmodzxznm  30748  zlmodzxzequap  30750  sec0  30804  elogb  30819  dalem-cly  32888  pmodN  33067  cdleme0cp  33431  cdleme0cq  33432  cdleme1  33444  cdleme3d  33448  cdleme3h  33452  cdleme4  33455  cdleme5  33457  cdleme7a  33460  cdleme8  33467  cdleme9  33470  cdleme10  33471  cdleme11g  33482  cdleme15b  33492  cdleme21  33554  cdleme22e  33561  cdleme22eALTN  33562  cdleme23c  33568  cdleme25cv  33575  cdleme35b  33667  cdleme35c  33668  cdleme42a  33688  cdleme42d  33690  cdleme43aN  33706  cdlemeg46gfv  33747  cdlemk35  34129  dihjatcclem1  34636  lcdval2  34808  mapdpglem21  34910
  Copyright terms: Public domain W3C validator