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

Theorem oveq2i 6255
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 6252 . 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 1437  (class class class)co 6244
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2058  ax-ext 2403
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2410  df-cleq 2416  df-clel 2419  df-nfc 2553  df-rex 2715  df-rab 2718  df-v 3019  df-dif 3377  df-un 3379  df-in 3381  df-ss 3388  df-nul 3700  df-if 3850  df-sn 3937  df-pr 3939  df-op 3943  df-uni 4158  df-br 4362  df-iota 5503  df-fv 5547  df-ov 6247
This theorem is referenced by:  caov32  6449  caov4  6453  caov42  6455  seqomsuc  7124  oa1suc  7183  om1  7193  oe1  7195  oawordeulem  7205  oeoalem  7247  nnm1  7299  nnm2  7300  nneob  7303  omopthlem1  7306  mapsnconst  7467  mapsncnv  7468  map2xp  7690  cantnflt  8124  cnfcom2  8154  infxpenc  8395  infxpenc2  8399  ackbij1lem5  8600  alephom  8956  pwxpndom2  9036  adderpqlem  9325  addassnq  9329  mulcanenq  9331  distrnq  9332  ltanq  9342  ltexnq  9346  halfnq  9347  ltrnq  9350  archnq  9351  addclprlem2  9388  prlem934  9404  prlem936  9418  addcmpblnr  9439  mulcmpblnrlem  9440  ltsrpr  9447  m1p1sr  9462  m1m1sr  9463  0idsr  9467  1idsr  9468  00sr  9469  pn0sr  9471  recexsrlem  9473  mulgt0sr  9475  sqgt0sr  9476  mulresr  9509  axmulcom  9525  axmulass  9527  axdistr  9528  axi2m1  9529  ax1rid  9531  axcnre  9534  mul02lem1  9755  addid1  9759  add42iOLD  9801  negid  9867  negsub  9868  subneg  9869  negsubdii  9906  muleqadd  10202  crne0  10548  2p2e4  10673  3p2e5  10688  3p3e6  10689  4p2e6  10690  4p3e7  10691  4p4e8  10692  5p2e7  10693  5p3e8  10694  5p4e9  10695  5p5e10  10696  6p2e8  10697  6p3e9  10698  6p4e10  10699  7p2e9  10700  7p3e10  10701  8p2e10  10702  3t3e9  10708  8th4div3  10779  halfpm6th  10780  addltmul  10794  nn0n0n1ge2  10878  nneo  10965  zeo  10967  numsuc  11009  numltc  11017  numsucc  11023  numma  11028  nummul1c  11033  6p5lem  11046  4t3lem  11068  decbin2  11101  xmulmnf1  11508  fztp  11798  fzprval  11802  fztpval  11803  fzshftral  11828  fz0tp  11839  fzo01  11940  fzo12sn  11941  fzo13pr  11942  fzo0to2pr  11943  fzo0to3tp  11944  fzo0to42pr  11945  quoremz  12027  quoremnn0ALT  12029  intfrac2  12030  intfracq  12031  sqval  12279  sqrecii  12302  cu2  12318  i3  12321  i4  12322  binom2i  12329  binom3  12338  crreczi  12342  nn0opthlem1  12399  facp1  12409  faclbnd  12420  faclbnd2  12421  faclbnd4lem1  12423  faclbnd4lem4  12426  bcn1  12443  bcn2  12449  4bc3eq4  12458  4bc2eq6  12459  hashgadd  12501  hashxplem  12548  hashmap  12550  hashfun  12552  hashbclem  12558  fz1isolem  12567  ccatlid  12673  ccatrid  12674  ccats1val2  12701  ccat2s1p2  12703  wrdeqs1cat  12772  swrdccatin12lem3  12787  swrdccat3a  12791  cats1fvn  12895  cats1cat  12898  swrds2  12959  reim0  13120  cji  13161  sqrtm1  13278  absi  13288  rddif  13342  iseraltlem2  13687  iseralt  13689  fsump1i  13768  fsummulc2  13783  incexclem  13832  incexc  13833  arisum2  13857  geoihalfsum  13876  mertenslem1  13878  mertens  13880  risefall0lem  14017  risefac1  14024  fallfac1  14025  fallfacfwd  14027  bpoly0  14041  bpoly1  14042  bpolydiflem  14045  bpoly2  14048  bpoly3  14049  bpoly4  14050  fsumcube  14051  ef0lem  14071  ege2le3  14082  eft0val  14104  ef4p  14105  efgt1p2  14106  efgt1p  14107  tanval2  14125  efival  14144  ef01bndlem  14176  sin01bnd  14177  cos01bnd  14178  cos1bnd  14179  cos2bnd  14180  rpnnen2lem11  14215  sqr2irrlem  14238  odd2np1lem  14302  odd2np1  14303  oddp1even  14305  divalglem5OLD  14314  divalglem5  14315  divalglem6  14316  bits0  14339  0bits  14351  gcdaddmlem  14430  6gcd4e2  14440  lcmneg  14506  3lcm2e6woprm  14518  6lcm4e12  14519  3prm  14579  3lcm2e6  14619  phiprm  14663  eulerthlem2  14668  prmdiv  14671  opoe  14699  pythagtriplem12  14714  pythagtriplem14  14716  pcmpt  14775  pcfac  14782  prmpwdvds  14786  pockthi  14789  prmreclem2  14799  prmreclem6  14803  4sqlem5  14824  4sqlem13OLD  14839  4sqlem13  14845  modxai  14978  mod2xnegi  14981  gcdi  14983  decexp2  14985  numexpp1  14988  numexp2x  14989  decsplit0b  14990  decsplit1  14992  decsplit  14993  2exp6OLD  14997  2exp16  14999  prmlem0  15015  139prm  15033  163prm  15034  317prm  15035  631prm  15036  1259lem1  15040  1259lem3  15042  1259lem4  15043  1259lem5  15044  1259prm  15045  2503lem1  15046  2503lem2  15047  2503lem3  15048  2503prm  15049  4001lem1  15050  4001lem2  15051  4001lem3  15052  4001lem4  15053  ressinbas  15123  rcaninv  15637  rescfth  15780  xpccatid  16011  oduval  16314  oppgmnd  16943  psgnunilem2  17074  psgnunilem4  17076  psgnpmtr  17089  psgn0fv0  17090  psgnsn  17099  psgnprfval1  17101  lsmmod2  17264  efgi0  17308  efgi1  17309  efginvrel2  17315  efgsval2  17321  efgsp1  17325  efgredleme  17331  efgredlemc  17333  efgcpbllemb  17343  frgpnabllem1  17447  lt6abl  17467  gsumconstf  17506  gsum2dlem2  17541  pwsgsum  17549  fsfnn0gsumfsffz  17550  dprd0  17602  dprdf1  17604  dprd2da  17613  ablfac1lem  17639  pgpfac1lem3  17648  pgpfaclem1  17652  srgbinomlem4  17714  opprring  17797  mulgass3  17803  evlsval  18680  mpff  18694  ply1assa  18730  gsumply1subr  18765  ply1coe  18827  ply1coeOLD  18828  coe1fzgsumdlem  18833  coe1fzgsumd  18834  gsumply1eq  18837  evl1gsumdlem  18882  evl1gsumd  18883  xrsnsgrp  18942  znbas  19051  znzrh2  19053  dsmmval2  19236  frlmip  19273  matgsum  19399  madetsumid  19423  mdetrsca  19565  mdetrsca2  19566  mdettpos  19573  m2detleiblem2  19590  madugsum  19605  madurid  19606  cpmat  19670  pmatcollpwfi  19743  pmatcollpw3fi1lem1  19747  pm2mpval  19756  mp2pm2mplem5  19771  chpmat1dlem  19796  chpmat1d  19797  chpidmat  19808  cpmidpmat  19834  cpmadugsumfi  19838  chcoeffeqlem  19846  cayleyhamilton0  19850  cayleyhamiltonALT  19852  cayleyhamilton1  19853  restin  20119  imacmp  20349  concompcon  20384  uptx  20577  cnpflf2  20952  tmdgsum2  21048  tsmsres  21095  tsmsf1o  21096  tsmsmhm  21097  prdsxmet  21321  resspwsds  21324  prdsxmslem2  21481  metdcn2  21794  metdcn  21795  metdscn2  21811  metdscn2OLD  21826  iimulcn  21903  icchmeo  21906  xrhmeo  21911  cnrehmeo  21918  cnheiborlem  21919  evth  21924  evth2  21925  lebnumlem2  21927  lebnumlem2OLD  21930  reparphti  21965  pcoass  21992  pi1xfrcnv  22025  ipcau2  22145  minveclem4  22311  minveclem4OLD  22323  pjthlem1  22328  ovolunlem1a  22386  unmbl  22428  uniioombl  22484  iblitg  22663  dfitg  22664  itg0  22674  iblcnlem1  22682  itgcnlem  22684  itgabs  22729  limcdif  22768  limccnp  22783  limccnp2  22784  dvexp  22844  dvmptid  22848  dvmptc  22849  dvmptfsum  22864  dveflem  22868  dvsincos  22870  mvth  22881  dvlipcn  22883  dvivthlem1  22897  dvfsumle  22910  dvfsumlem2  22916  itgsubst  22938  tdeglem4  22946  tdeglem2  22947  plypf1  23103  plymullem1  23105  coesub  23148  dgrmulc  23162  fta1lem  23197  vieta1lem1  23200  vieta1lem2  23201  aalioulem4  23228  aaliou3lem3  23237  abelthlem2  23324  abelthlem8  23331  abelthlem9  23332  sinhalfpilem  23355  efhalfpi  23363  cospi  23364  efipi  23365  sin2pi  23367  cos2pi  23368  ef2pi  23369  sin2pim  23377  cos2pim  23378  sinmpi  23379  cosmpi  23380  sinppi  23381  cosppi  23382  sincosq4sgn  23393  tangtx  23397  sincos4thpi  23405  sincos6thpi  23407  sincos3rdpi  23408  pige3  23409  abssinper  23410  efif1olem4  23431  efifo  23433  eff1o  23435  circgrp  23438  circsubm  23439  logneg  23474  logimul  23500  logneg2  23501  dvrelog  23519  logcnlem4  23527  dvlog  23533  dvlog2  23535  logtayl  23542  1cxp  23554  ecxp  23555  cxpsqrt  23585  dvsqrt  23619  dvcnsqrt  23621  root1eq1  23632  cxpeq  23634  elogb  23644  ang180lem1  23675  ang180lem2  23676  heron  23701  1cubrlem  23704  1cubr  23705  dcubic2  23707  mcubic  23710  cubic2  23711  binom4  23713  dquartlem1  23714  dquartlem2  23715  dquart  23716  quart1lem  23718  quart1  23719  quartlem1  23720  asinsin  23755  asin1  23757  acos1  23758  atanlogsublem  23778  atanlogsub  23779  efiatan2  23780  2efiatan  23781  tanatan  23782  atanbnd  23789  atan1  23791  dvatan  23798  atantayl2  23801  leibpilem2  23804  leibpi  23805  log2cnv  23807  log2tlbnd  23808  log2ublem1  23809  log2ublem2  23810  log2ublem3  23811  log2ub  23812  birthday  23817  amgmlem  23852  emcllem5  23862  lgamgulmlem2  23892  lgamgulmlem5  23895  lgam1  23926  wilthlem2  23931  ftalem6  23941  basellem2  23945  basellem3  23946  basellem5  23948  basellem8  23951  cht1  24029  chp1  24031  1sgmprm  24064  ppiublem2  24068  ppiub  24069  chtublem  24076  chtub  24077  logfacbnd3  24088  bcp1ctr  24144  bclbnd  24145  bposlem1  24149  bposlem4  24152  bposlem6  24154  bposlem8  24156  bposlem9  24157  lgslem1  24161  lgsdir2lem1  24188  lgsdir2lem2  24189  lgsdir2lem3  24190  lgsdir2lem5  24192  lgs1  24203  lgseisenlem1  24214  lgseisenlem3  24216  lgsquadlem1  24219  lgsquadlem2  24220  lgsquad2lem2  24224  m1lgs  24227  2sqlem8  24237  2sqblem  24242  logdivsum  24308  mulog2sumlem2  24310  log2sumbnd  24319  selberglem1  24320  selberglem2  24321  pntrmax  24339  pntibndlem2  24366  pntibndlem3  24367  pntlemg  24373  pntlemr  24377  pntlemo  24382  ostth2lem3  24410  ostth2lem4  24411  istrkg3ld  24446  trgcgrg  24497  tgcgr4  24513  colperpexlem1  24709  ax5seglem7  24902  axlowdimlem4  24912  axlowdimlem16  24924  0wlk  25212  0trl  25213  wlkntrllem2  25227  wlkntrl  25229  constr1trl  25255  1pthonlem1  25256  constr2wlk  25265  constr2trl  25266  wlkdvspthlem  25274  constr3trllem3  25317  constr3trllem4  25318  constr3trllem5  25319  constr3pthlem1  25320  constr3pthlem3  25322  clwwlkn2  25440  clwlkisclwwlk2  25455  wwlkext2clwwlk  25468  vdgr1c  25570  nbhashuvtx1  25580  vdegp1ai  25649  vdegp1bi  25650  vdegp1ci  25651  extwwlkfablem2  25743  numclwwlkovf2ex  25751  numclwlk2lem2f  25768  frgraregord013  25783  ex-ind-dvds  25836  smcnlem  26270  ipidsq  26286  dipcj  26290  dip0r  26293  nmlnoubi  26374  nmblolbii  26377  blocnilem  26382  ip1ilem  26404  ip2i  26406  ipdirilem  26407  ipasslem10  26417  ipasslem11  26418  siilem1  26429  hvmul0  26614  hvsubsub4i  26649  hvnegdii  26652  hvsubeq0i  26653  hvsubcan2i  26654  hvsubaddi  26656  hvsub0  26666  hisubcomi  26694  normlem0  26699  normlem1  26700  normlem2  26701  normlem3  26702  normlem9  26708  norm-ii-i  26727  norm3difi  26737  normpari  26744  polid2i  26747  polidi  26748  bcsiALT  26769  pjhthlem1  26981  chdmm3i  27069  chdmm4i  27070  chjidm  27110  chj4i  27113  chjjdiri  27114  spanunsni  27169  pjoml4i  27177  cmcm2i  27183  qlax4i  27220  qlax5i  27221  pjadjii  27264  pjmulii  27267  pjsubii  27268  pjssmii  27271  pjcji  27274  pjneli  27313  hoadd32i  27368  ho0subi  27385  hosubid1  27388  hosd2i  27413  hopncani  27414  hosubeq0i  27416  lnopeq0lem1  27595  lnopunilem1  27600  lnophmlem2  27607  nmbdoplbi  27614  nmcopexi  27617  lnfnmuli  27634  nmcfnexi  27641  nmoptri2i  27689  nmopcoadji  27691  golem1  27861  mdsl1i  27911  cvmdi  27914  mdslmd3i  27922  csmdsymi  27924  xrge00  28394  archirngz  28452  archiabllem2c  28458  gsumle  28488  gsummpt2co  28489  gsumvsca1  28492  gsumvsca2  28493  xrge0slmod  28554  psgnfzto1st  28565  lmat22det  28595  madjusmdetlem4  28603  raddcn  28682  xrge0iifhom  28690  xrge0mulc1cn  28694  cbvesum  28810  gsumesum  28827  esumpfinvallem  28842  esumpfinvalf  28844  dya2icoseg  29046  sitg0  29126  eulerpartlemd  29146  eulerpartlemgvv  29156  eulerpartlemgh  29158  fib0  29179  fib1  29180  fibp1  29181  orrvcval4  29244  orrvcoel  29245  orrvccel  29246  coinflipprob  29259  coinflippvt  29264  ballotlem2  29268  ballotth  29317  ballotthOLD  29355  signstf0  29404  signstfvn  29405  signsvtn0  29406  signstfvp  29407  signstfveq0  29413  signsvf0  29416  signsvf1  29417  signsvfn  29418  signshf  29424  subfacp1lem1  29849  subfacp1lem5  29854  subfacval2  29857  subfaclim  29858  subfacval3  29859  cvxpcon  29912  cvxscon  29913  mrsub0  30101  problem4  30247  quad3  30249  sinccvglem  30263  iexpire  30317  faclimlem1  30325  frrlem5  30464  fwddifnp1  30876  finxpreclem4  31693  ptrest  31846  poimirlem25  31872  poimirlem27  31874  dvtan  31899  itgabsnc  31918  ftc1anclem8  31931  dvasin  31935  dvacos  31936  areacirclem1  31939  areacirclem4  31942  areacirc  31944  prdstotbnd  32033  prdsbnd2  32034  repwsmet  32073  rrnequiv  32074  reheibor  32078  dalem-cly  33148  pmodN  33327  cdleme0cp  33692  cdleme0cq  33693  cdleme1  33705  cdleme3d  33709  cdleme3h  33713  cdleme4  33716  cdleme5  33718  cdleme7a  33721  cdleme8  33728  cdleme9  33731  cdleme10  33732  cdleme11g  33743  cdleme15b  33753  cdleme21  33816  cdleme22e  33823  cdleme22eALTN  33824  cdleme23c  33830  cdleme25cv  33837  cdleme35b  33929  cdleme35c  33930  cdleme42a  33950  cdleme42d  33952  cdleme43aN  33968  cdlemeg46gfv  34009  cdlemk35  34391  dihjatcclem1  34898  lcdval2  35070  mapdpglem21  35172  mapfzcons  35470  mapfzcons1cl  35472  2rexfrabdioph  35551  3rexfrabdioph  35552  4rexfrabdioph  35553  6rexfrabdioph  35554  7rexfrabdioph  35555  rabdiophlem2  35557  diophren  35568  rabren3dioph  35570  pellexlem5  35590  pell1qr1  35630  rmspecfund  35670  jm2.17a  35723  jm2.17b  35724  jm2.27c  35775  jm2.27dlem5  35781  lmhmlnmsplit  35858  arearect  36013  areaquad  36014  relexp2  36182  trclfvdecomr  36233  inductionexd  36506  unitadd  36555  amgm2d  36563  amgm3d  36564  lhe4.4ex1a  36591  expgrowthi  36595  expgrowth  36597  bccn1  36606  binomcxplemdvbinom  36615  binomcxplemdvsum  36617  binomcxplemnotnn0  36618  binomcxp  36619  refsumcn  37267  oddfl  37384  m1expevenOLD  37553  sumnnodd  37593  cosnegpi  37625  dvcosre  37664  dvsinax  37666  ioodvbdlimc1lem2  37687  ioodvbdlimc1lem2OLD  37689  ioodvbdlimc2lem  37691  ioodvbdlimc2lemOLD  37692  dvmptmulf  37695  dvxpaek  37698  dvmptfprod  37703  dvnprodlem2  37705  dvnprodlem3  37706  itgsin0pilem1  37709  itgsinexplem1  37713  itgsubsticclem  37735  stoweidlem13  37756  wallispilem4  37813  wallispi2lem1  37816  wallispi2lem2  37817  stirlinglem1  37819  dirkerper  37841  dirkertrigeqlem1  37843  dirkertrigeqlem3  37845  dirkertrigeq  37846  dirkeritg  37847  dirkercncflem1  37848  dirkercncflem2  37849  fourierdlem36  37889  fourierdlem41  37894  fourierdlem42  37895  fourierdlem42OLD  37896  fourierdlem48  37901  fourierdlem56  37909  fourierdlem57  37910  fourierdlem58  37911  fourierdlem60  37913  fourierdlem61  37914  fourierdlem62  37915  fourierdlem65  37918  fourierdlem73  37926  fourierdlem80  37933  fourierdlem87  37940  fourierdlem89  37942  fourierdlem90  37943  fourierdlem91  37944  fourierdlem100  37953  fourierdlem103  37956  fourierdlem107  37960  fourierdlem112  37965  fourierdlem113  37966  fourierdlem115  37968  fouriercnp  37973  sqwvfoura  37975  sqwvfourb  37976  fourierswlem  37977  fouriersw  37978  etransclem2  37984  etransclem37  38019  etransclem46  38028  hoidmvlelem3  38266  1t10e1p1e11  38523  deccarry  38528  bits0ALTV  38621  nnsum3primes4  38696  nnsum3primesgbe  38700  nnsum4primesodd  38704  nnsum4primesoddALTV  38705  nnsum4primeseven  38708  nnsum4primesevenALTV  38709  bgoldbtbndlem1  38713  tgoldbachlt  38722  5tcu2e40  38728  3exp4mod41  38729  41prothprmlem1  38730  41prothprmlem2  38731  41prothprm  38732  pfx1  38765  pfxccatpfx1  38781  pfxccatpfx2  38782  uhgrepe  39281  2t6m3t4e0  39722  zlmodzxzequa  39882  zlmodzxznm  39883  zlmodzxzequap  39885  nn0sumshdiglemA  40023  nn0sumshdiglemB  40024  nn0sumshdiglem1  40025  sec0  40073
  Copyright terms: Public domain W3C validator