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

Theorem oveq2i 6097
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 6094 . 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 1369  (class class class)co 6086
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-rex 2716  df-rab 2719  df-v 2969  df-dif 3326  df-un 3328  df-in 3330  df-ss 3337  df-nul 3633  df-if 3787  df-sn 3873  df-pr 3875  df-op 3879  df-uni 4087  df-br 4288  df-iota 5376  df-fv 5421  df-ov 6089
This theorem is referenced by:  caov32  6285  caov4  6289  caov42  6291  seqomsuc  6904  oa1suc  6963  om1  6973  oe1  6975  oawordeulem  6985  oeoalem  7027  nnm1  7079  nnm2  7080  nneob  7083  omopthlem1  7086  mapsnconst  7250  mapsncnv  7251  map2xp  7473  cantnflt  7872  cantnfltOLD  7902  cnfcom2  7927  cnfcom2OLD  7935  infxpenc  8176  infxpenc2  8180  infxpencOLD  8181  infxpenc2OLD  8184  ackbij1lem5  8385  alephom  8741  pwxpndom2  8824  adderpqlem  9115  addassnq  9119  mulcanenq  9121  distrnq  9122  ltanq  9132  ltexnq  9136  halfnq  9137  ltrnq  9140  archnq  9141  addclprlem2  9178  prlem934  9194  prlem936  9208  addcmpblnr  9231  mulcmpblnrlem  9232  ltsrpr  9236  m1p1sr  9251  m1m1sr  9252  0idsr  9256  1idsr  9257  00sr  9258  pn0sr  9260  recexsrlem  9262  mulgt0sr  9264  sqgt0sr  9265  mulresr  9298  axmulcom  9314  axmulass  9316  axdistr  9317  axi2m1  9318  ax1rid  9320  axcnre  9323  mul02lem1  9537  addid1  9541  add42i  9582  negid  9648  negsub  9649  subneg  9650  negsubdii  9685  muleqadd  9972  crne0  10307  2p2e4  10431  3p2e5  10446  3p3e6  10447  4p2e6  10448  4p3e7  10449  4p4e8  10450  5p2e7  10451  5p3e8  10452  5p4e9  10453  5p5e10  10454  6p2e8  10455  6p3e9  10456  6p4e10  10457  7p2e9  10458  7p3e10  10459  8p2e10  10460  3t3e9  10466  8th4div3  10537  halfpm6th  10538  addltmul  10552  nn0n0n1ge2  10635  nneo  10717  zeo  10719  numsuc  10759  numltc  10767  numsucc  10773  numma  10778  nummul1c  10783  6p5lem  10796  4t3lem  10818  decbin2  10851  xmulmnf1  11231  fztp  11504  fz0tp  11505  fzprval  11509  fztpval  11510  fzshftral  11539  fzo01  11604  fzo12sn  11605  fzo0to2pr  11606  fzo0to3tp  11607  fzo0to42pr  11608  quoremz  11686  quoremnn0ALT  11688  intfrac2  11689  intfracq  11690  sqval  11917  sqrecii  11940  cu2  11956  i3  11959  i4  11960  binom2i  11967  binom3  11977  crreczi  11981  nn0opthlem1  12038  facp1  12048  faclbnd  12058  faclbnd2  12059  faclbnd4lem1  12061  faclbnd4lem4  12064  bcn1  12081  bcn2  12087  hashgadd  12132  hashxplem  12187  hashmap  12189  hashfun  12191  hashbclem  12197  fz1isolem  12206  ccatlid  12276  ccatrid  12277  eqs1  12292  ccats1val2  12299  wrdeqs1cat  12361  cats1un  12362  swrdccatin12lem3  12373  swrdccat3a  12377  cats1fvn  12477  cats1cat  12480  swrds2  12537  reim0  12599  cji  12640  sqrm1  12757  absi  12767  rddif  12820  iseraltlem2  13152  iseralt  13154  fsump1i  13228  fsummulc2  13243  incexclem  13291  incexc  13292  arisum2  13315  geoihalfsum  13334  mertenslem1  13336  mertens  13338  ef0lem  13356  ege2le3  13367  eft0val  13388  ef4p  13389  efgt1p2  13390  efgt1p  13391  tanval2  13409  efival  13428  ef01bndlem  13460  sin01bnd  13461  cos01bnd  13462  cos1bnd  13463  cos2bnd  13464  rpnnen2lem11  13499  sqr2irrlem  13522  odd2np1lem  13583  odd2np1  13584  oddp1even  13586  divalglem5  13593  divalglem6  13594  bits0  13616  0bits  13627  gcdaddmlem  13704  3prm  13772  phiprm  13844  eulerthlem2  13849  prmdiv  13852  opoe  13870  pythagtriplem12  13885  pythagtriplem14  13887  pcmpt  13946  pcfac  13953  prmpwdvds  13957  pockthi  13960  prmreclem2  13970  prmreclem6  13974  4sqlem5  13995  4sqlem13  14010  modxai  14089  mod2xnegi  14092  gcdi  14094  decexp2  14096  numexpp1  14099  numexp2x  14100  decsplit0b  14101  decsplit1  14103  decsplit  14104  2exp6  14107  2exp16  14109  prmlem0  14125  139prm  14143  163prm  14144  317prm  14145  631prm  14146  1259lem1  14147  1259lem3  14149  1259lem4  14150  1259lem5  14151  1259prm  14152  2503lem1  14153  2503lem2  14154  2503lem3  14155  2503prm  14156  4001lem1  14157  4001lem2  14158  4001lem3  14159  4001lem4  14160  ressinbas  14226  rescfth  14839  xpccatid  14990  oduval  15292  oppgmnd  15860  psgnunilem2  15992  psgnunilem4  15994  psgnpmtr  16007  psgn0fv0  16008  psgnprfval1  16017  lsmmod2  16164  efgi0  16208  efgi1  16209  efginvrel2  16215  efgsval2  16221  efgsp1  16225  efgredleme  16231  efgredlemc  16233  efgcpbllemb  16243  frgpnabllem1  16342  lt6abl  16362  gsumconstf  16418  gsumsn  16439  gsum2dlem2  16450  gsum2dOLD  16452  pwsgsum  16461  pwsgsumOLD  16462  dprd0  16516  dprdf1  16518  dprd2da  16529  ablfac1lem  16557  pgpfac1lem3  16566  pgpfaclem1  16570  srgbinomlem4  16629  opprrng  16711  mulgass3  16717  evlsval  17580  mpff  17594  ply1assa  17630  gsumply1subr  17663  ply1coe  17721  ply1coeOLD  17722  evl1gsumdlem  17765  evl1gsumd  17766  znbas  17951  znzrh2  17953  dsmmval2  18136  frlmip  18178  madetsumid  18321  mdetrsca  18385  mdetrsca2  18386  mdettpos  18392  m2detleiblem2  18409  madugsum  18424  madurid  18425  restin  18745  imacmp  18975  concompcon  19011  uptx  19173  cnpflf2  19548  tmdgsum2  19642  tsmsresOLD  19692  tsmsres  19693  tsmsf1o  19694  tsmsmhm  19695  prdsxmet  19919  resspwsds  19922  prdsxmslem2  20079  metdcn2  20391  metdcn  20392  metdscn2  20408  iimulcn  20485  icchmeo  20488  xrhmeo  20493  cnrehmeo  20500  cnheiborlem  20501  evth  20506  evth2  20507  lebnumlem2  20509  reparphti  20544  pcoass  20571  pi1xfrcnv  20604  ipcau2  20724  minveclem4  20894  pjthlem1  20899  ovolunlem1a  20954  unmbl  20994  uniioombl  21044  iblitg  21221  dfitg  21222  itg0  21232  iblcnlem1  21240  itgcnlem  21242  itgabs  21287  limcdif  21326  limccnp  21341  limccnp2  21342  dvexp  21402  dvmptid  21406  dvmptc  21407  dvmptfsum  21422  dveflem  21426  dvsincos  21428  mvth  21439  dvlipcn  21441  dvivthlem1  21455  dvfsumle  21468  dvfsumlem2  21474  itgsubst  21496  tdeglem4  21504  tdeglem2  21505  plypf1  21655  plymullem1  21657  coesub  21699  dgrmulc  21713  fta1lem  21748  vieta1lem1  21751  vieta1lem2  21752  aalioulem4  21776  aaliou3lem3  21785  abelthlem2  21872  abelthlem8  21879  abelthlem9  21880  sinhalfpilem  21900  efhalfpi  21908  cospi  21909  efipi  21910  sin2pi  21912  cos2pi  21913  ef2pi  21914  sin2pim  21922  cos2pim  21923  sinmpi  21924  cosmpi  21925  sinppi  21926  cosppi  21927  sincosq4sgn  21938  tangtx  21942  sincos4thpi  21950  sincos6thpi  21952  sincos3rdpi  21953  pige3  21954  abssinper  21955  efif1olem4  21976  efifo  21978  eff1o  21980  logneg  22011  logimul  22038  logneg2  22039  dvrelog  22057  logcnlem4  22065  dvlog  22071  dvlog2  22073  logtayl  22080  1cxp  22092  ecxp  22093  cxpsqr  22123  dvsqr  22157  root1eq1  22168  cxpeq  22170  ang180lem1  22180  ang180lem2  22181  heron  22208  1cubrlem  22211  1cubr  22212  dcubic2  22214  mcubic  22217  cubic2  22218  binom4  22220  dquartlem1  22221  dquartlem2  22222  dquart  22223  quart1lem  22225  quart1  22226  quartlem1  22227  asinsin  22262  asin1  22264  acos1  22265  atanlogsublem  22285  atanlogsub  22286  efiatan2  22287  2efiatan  22288  tanatan  22289  atanbnd  22296  atan1  22298  dvatan  22305  atantayl2  22308  leibpilem2  22311  leibpi  22312  log2cnv  22314  log2tlbnd  22315  log2ublem1  22316  log2ublem2  22317  log2ublem3  22318  log2ub  22319  birthday  22323  amgmlem  22358  emcllem5  22368  wilthlem2  22382  ftalem6  22390  basellem2  22394  basellem3  22395  basellem5  22397  basellem8  22400  cht1  22478  chp1  22480  1sgmprm  22513  ppiublem2  22517  ppiub  22518  chtublem  22525  chtub  22526  logfacbnd3  22537  bcp1ctr  22593  bclbnd  22594  bposlem1  22598  bposlem4  22601  bposlem6  22603  bposlem8  22605  bposlem9  22606  lgslem1  22610  lgsdir2lem1  22637  lgsdir2lem2  22638  lgsdir2lem3  22639  lgsdir2lem5  22641  lgs1  22652  lgseisenlem1  22663  lgseisenlem3  22665  lgsquadlem1  22668  lgsquadlem2  22669  lgsquad2lem2  22673  m1lgs  22676  2sqlem8  22686  2sqblem  22691  logdivsum  22757  mulog2sumlem2  22759  log2sumbnd  22768  selberglem1  22769  selberglem2  22770  pntrmax  22788  pntibndlem2  22815  pntibndlem3  22816  pntlemg  22822  pntlemr  22826  pntlemo  22831  ostth2lem3  22859  ostth2lem4  22860  trgcgrg  22942  ax5seglem7  23132  axlowdimlem4  23142  axlowdimlem16  23154  0wlk  23395  0trl  23396  wlkntrllem2  23410  wlkntrl  23412  constr1trl  23438  1pthonlem1  23439  constr2wlk  23448  constr2trl  23449  wlkdvspthlem  23457  constr3trllem3  23489  constr3trllem4  23490  constr3trllem5  23491  constr3pthlem1  23492  constr3pthlem3  23494  vdgr1c  23526  vdegp1ai  23556  vdegp1bi  23557  vdegp1ci  23558  smcnlem  24043  ipidsq  24059  dipcj  24063  dip0r  24066  nmlnoubi  24147  nmblolbii  24150  blocnilem  24155  ip1ilem  24177  ip2i  24179  ipdirilem  24180  ipasslem10  24190  ipasslem11  24191  siilem1  24202  hvmul0  24377  hvsubsub4i  24412  hvnegdii  24415  hvsubeq0i  24416  hvsubcan2i  24417  hvsubaddi  24419  hvsub0  24429  hisubcomi  24457  normlem0  24462  normlem1  24463  normlem2  24464  normlem3  24465  normlem9  24471  norm-ii-i  24490  norm3difi  24500  normpari  24507  polid2i  24510  polidi  24511  bcsiALT  24532  pjhthlem1  24745  chdmm3i  24833  chdmm4i  24834  chjidm  24874  chj4i  24877  chjjdiri  24878  spanunsni  24933  pjoml4i  24941  cmcm2i  24947  qlax4i  24984  qlax5i  24985  pjadjii  25028  pjmulii  25031  pjsubii  25032  pjssmii  25035  pjcji  25038  pjneli  25077  hoadd32i  25133  ho0subi  25150  hosubid1  25153  hosd2i  25178  hopncani  25179  hosubeq0i  25181  lnopeq0lem1  25360  lnopunilem1  25365  lnophmlem2  25372  nmbdoplbi  25379  nmcopexi  25382  lnfnmuli  25399  nmcfnexi  25406  nmoptri2i  25454  nmopcoadji  25456  golem1  25626  mdsl1i  25676  cvmdi  25679  mdslmd3i  25687  csmdsymi  25689  xrge00  26098  archirngz  26157  archiabllem2c  26163  gsumsnf  26195  gsumle  26197  gsummptun  26199  gsumvsca1  26202  gsumvsca2  26203  xrge0slmod  26264  raddcn  26311  xrge0iifhom  26319  xrge0mulc1cn  26323  cbvesum  26449  gsumesum  26462  esumpfinvallem  26475  esumpfinvalf  26477  dya2icoseg  26644  sitg0  26684  eulerpartlemd  26701  eulerpartlemgvv  26711  eulerpartlemgh  26713  fib0  26734  fib1  26735  fibp1  26736  orrvcval4  26799  orrvcoel  26800  orrvccel  26801  coinflipprob  26814  coinflippvt  26819  ballotlem2  26823  ballotth  26872  signstf0  26921  signstfvn  26922  signsvtn0  26923  signstfvp  26924  signstfvneq0  26925  signstfveq0  26930  signsvf0  26933  signsvf1  26934  signsvfn  26935  signshf  26941  lgamgulmlem2  26968  lgamgulmlem5  26971  lgam1  27002  subfacp1lem1  27019  subfacp1lem5  27024  subfacval2  27027  subfaclim  27028  subfacval3  27029  cvxpcon  27083  cvxscon  27084  problem4  27253  sinccvglem  27268  4bc3eq4  27341  4bc2eq6  27342  risefall0lem  27480  risefac1  27487  fallfac1  27488  fallfacfwd  27490  faclimlem1  27500  frrlem5  27723  bpoly0  28144  bpoly1  28145  bpolydiflem  28148  bpoly2  28151  bpoly3  28152  bpoly4  28153  fsumcube  28154  ptrest  28378  dvtan  28395  itgabsnc  28414  ftc1anclem8  28427  dvcnsqr  28431  dvasin  28433  dvacos  28434  areacirclem1  28437  areacirclem4  28440  areacirc  28442  prdstotbnd  28646  prdsbnd2  28647  repwsmet  28686  rrnequiv  28687  reheibor  28691  mapfzcons  29005  mapfzcons1cl  29007  2rexfrabdioph  29087  3rexfrabdioph  29088  4rexfrabdioph  29089  6rexfrabdioph  29090  7rexfrabdioph  29091  rabdiophlem2  29093  diophren  29105  rabren3dioph  29107  pellexlem5  29127  pell1qr1  29165  rmspecfund  29203  jm2.17a  29256  jm2.17b  29257  jm2.27c  29309  jm2.27dlem5  29315  lmhmlnmsplit  29393  arearect  29544  areaquad  29545  lhe4.4ex1a  29556  expgrowthi  29560  expgrowth  29562  refsumcn  29705  m1expeven  29725  dvcosre  29741  itgsin0pilem1  29743  itgsinexplem1  29747  stoweidlem13  29761  wallispilem4  29816  wallispi2lem1  29819  wallispi2lem2  29820  stirlinglem1  29822  f13idfv  30101  ccat2s1p2  30219  ccatw2s1p2  30223  clwwlkn2  30391  clwlkisclwwlk2  30405  wwlkext2clwwlk  30418  nbhashuvtx1  30486  extwwlkfablem2  30624  numclwwlkovf2ex  30632  numclwlk2lem2f  30649  frgraregord013  30664  2t6m3t4e0  30692  psgnsn  30722  matgsum  30785  zlmodzxzequa  30927  zlmodzxznm  30928  zlmodzxzequap  30930  sec0  30984  elogb  30999  dalem-cly  33155  pmodN  33334  cdleme0cp  33698  cdleme0cq  33699  cdleme1  33711  cdleme3d  33715  cdleme3h  33719  cdleme4  33722  cdleme5  33724  cdleme7a  33727  cdleme8  33734  cdleme9  33737  cdleme10  33738  cdleme11g  33749  cdleme15b  33759  cdleme21  33821  cdleme22e  33828  cdleme22eALTN  33829  cdleme23c  33835  cdleme25cv  33842  cdleme35b  33934  cdleme35c  33935  cdleme42a  33955  cdleme42d  33957  cdleme43aN  33973  cdlemeg46gfv  34014  cdlemk35  34396  dihjatcclem1  34903  lcdval2  35075  mapdpglem21  35177
  Copyright terms: Public domain W3C validator