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

Theorem oveq2i 6316
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 6313 . 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 6305
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-rex 2788  df-rab 2791  df-v 3089  df-dif 3445  df-un 3447  df-in 3449  df-ss 3456  df-nul 3768  df-if 3916  df-sn 4003  df-pr 4005  df-op 4009  df-uni 4223  df-br 4427  df-iota 5565  df-fv 5609  df-ov 6308
This theorem is referenced by:  caov32  6510  caov4  6514  caov42  6516  seqomsuc  7182  oa1suc  7241  om1  7251  oe1  7253  oawordeulem  7263  oeoalem  7305  nnm1  7357  nnm2  7358  nneob  7361  omopthlem1  7364  mapsnconst  7525  mapsncnv  7526  map2xp  7748  cantnflt  8176  cnfcom2  8206  infxpenc  8447  infxpenc2  8451  ackbij1lem5  8652  alephom  9008  pwxpndom2  9089  adderpqlem  9378  addassnq  9382  mulcanenq  9384  distrnq  9385  ltanq  9395  ltexnq  9399  halfnq  9400  ltrnq  9403  archnq  9404  addclprlem2  9441  prlem934  9457  prlem936  9471  addcmpblnr  9492  mulcmpblnrlem  9493  ltsrpr  9500  m1p1sr  9515  m1m1sr  9516  0idsr  9520  1idsr  9521  00sr  9522  pn0sr  9524  recexsrlem  9526  mulgt0sr  9528  sqgt0sr  9529  mulresr  9562  axmulcom  9578  axmulass  9580  axdistr  9581  axi2m1  9582  ax1rid  9584  axcnre  9587  mul02lem1  9808  addid1  9812  add42iOLD  9854  negid  9920  negsub  9921  subneg  9922  negsubdii  9959  muleqadd  10255  crne0  10602  2p2e4  10727  3p2e5  10742  3p3e6  10743  4p2e6  10744  4p3e7  10745  4p4e8  10746  5p2e7  10747  5p3e8  10748  5p4e9  10749  5p5e10  10750  6p2e8  10751  6p3e9  10752  6p4e10  10753  7p2e9  10754  7p3e10  10755  8p2e10  10756  3t3e9  10762  8th4div3  10833  halfpm6th  10834  addltmul  10848  nn0n0n1ge2  10932  nneo  11019  zeo  11021  numsuc  11063  numltc  11071  numsucc  11077  numma  11082  nummul1c  11087  6p5lem  11100  4t3lem  11122  decbin2  11155  xmulmnf1  11562  fztp  11850  fzprval  11854  fztpval  11855  fzshftral  11880  fz0tp  11891  fzo01  11992  fzo12sn  11993  fzo13pr  11994  fzo0to2pr  11995  fzo0to3tp  11996  fzo0to42pr  11997  quoremz  12079  quoremnn0ALT  12081  intfrac2  12082  intfracq  12083  sqval  12331  sqrecii  12354  cu2  12370  i3  12373  i4  12374  binom2i  12381  binom3  12390  crreczi  12394  nn0opthlem1  12451  facp1  12461  faclbnd  12472  faclbnd2  12473  faclbnd4lem1  12475  faclbnd4lem4  12478  bcn1  12495  bcn2  12501  4bc3eq4  12510  4bc2eq6  12511  hashgadd  12553  hashxplem  12600  hashmap  12602  hashfun  12604  hashbclem  12610  fz1isolem  12619  ccatlid  12717  ccatrid  12718  ccats1val2  12745  ccat2s1p2  12747  wrdeqs1cat  12816  swrdccatin12lem3  12831  swrdccat3a  12835  cats1fvn  12939  cats1cat  12942  swrds2  12999  reim0  13160  cji  13201  sqrtm1  13318  absi  13328  rddif  13382  iseraltlem2  13727  iseralt  13729  fsump1i  13808  fsummulc2  13823  incexclem  13872  incexc  13873  arisum2  13897  geoihalfsum  13916  mertenslem1  13918  mertens  13920  risefall0lem  14057  risefac1  14064  fallfac1  14065  fallfacfwd  14067  bpoly0  14081  bpoly1  14082  bpolydiflem  14085  bpoly2  14088  bpoly3  14089  bpoly4  14090  fsumcube  14091  ef0lem  14111  ege2le3  14122  eft0val  14144  ef4p  14145  efgt1p2  14146  efgt1p  14147  tanval2  14165  efival  14184  ef01bndlem  14216  sin01bnd  14217  cos01bnd  14218  cos1bnd  14219  cos2bnd  14220  rpnnen2lem11  14255  sqr2irrlem  14278  odd2np1lem  14342  odd2np1  14343  oddp1even  14345  divalglem5  14353  divalglem6  14354  bits0  14376  0bits  14387  gcdaddmlem  14466  6gcd4e2  14476  lcmneg  14533  3lcm2e6woprm  14545  6lcm4e12  14546  3prm  14603  3lcm2e6  14643  phiprm  14685  eulerthlem2  14690  prmdiv  14693  opoe  14715  pythagtriplem12  14730  pythagtriplem14  14732  pcmpt  14791  pcfac  14798  prmpwdvds  14802  pockthi  14805  prmreclem2  14815  prmreclem6  14819  4sqlem5  14840  4sqlem13OLD  14855  4sqlem13  14861  modxai  14994  mod2xnegi  14997  gcdi  14999  decexp2  15001  numexpp1  15004  numexp2x  15005  decsplit0b  15006  decsplit1  15008  decsplit  15009  2exp6OLD  15013  2exp16  15015  prmlem0  15031  139prm  15049  163prm  15050  317prm  15051  631prm  15052  1259lem1  15056  1259lem3  15058  1259lem4  15059  1259lem5  15060  1259prm  15061  2503lem1  15062  2503lem2  15063  2503lem3  15064  2503prm  15065  4001lem1  15066  4001lem2  15067  4001lem3  15068  4001lem4  15069  ressinbas  15138  rcaninv  15641  rescfth  15784  xpccatid  16015  oduval  16318  oppgmnd  16947  psgnunilem2  17078  psgnunilem4  17080  psgnpmtr  17093  psgn0fv0  17094  psgnsn  17103  psgnprfval1  17105  lsmmod2  17252  efgi0  17296  efgi1  17297  efginvrel2  17303  efgsval2  17309  efgsp1  17313  efgredleme  17319  efgredlemc  17321  efgcpbllemb  17331  frgpnabllem1  17435  lt6abl  17455  gsumconstf  17494  gsum2dlem2  17529  pwsgsum  17537  fsfnn0gsumfsffz  17538  dprd0  17590  dprdf1  17592  dprd2da  17601  ablfac1lem  17627  pgpfac1lem3  17636  pgpfaclem1  17640  srgbinomlem4  17702  opprring  17785  mulgass3  17791  evlsval  18668  mpff  18682  ply1assa  18718  gsumply1subr  18753  ply1coe  18815  ply1coeOLD  18816  coe1fzgsumdlem  18821  coe1fzgsumd  18822  gsumply1eq  18825  evl1gsumdlem  18870  evl1gsumd  18871  xrsnsgrp  18930  znbas  19036  znzrh2  19038  dsmmval2  19221  frlmip  19258  matgsum  19384  madetsumid  19408  mdetrsca  19550  mdetrsca2  19551  mdettpos  19558  m2detleiblem2  19575  madugsum  19590  madurid  19591  cpmat  19655  pmatcollpwfi  19728  pmatcollpw3fi1lem1  19732  pm2mpval  19741  mp2pm2mplem5  19756  chpmat1dlem  19781  chpmat1d  19782  chpidmat  19793  cpmidpmat  19819  cpmadugsumfi  19823  chcoeffeqlem  19831  cayleyhamilton0  19835  cayleyhamiltonALT  19837  cayleyhamilton1  19838  restin  20104  imacmp  20334  concompcon  20369  uptx  20562  cnpflf2  20937  tmdgsum2  21033  tsmsres  21080  tsmsf1o  21081  tsmsmhm  21082  prdsxmet  21306  resspwsds  21309  prdsxmslem2  21466  metdcn2  21759  metdcn  21760  metdscn2  21776  iimulcn  21853  icchmeo  21856  xrhmeo  21861  cnrehmeo  21868  cnheiborlem  21869  evth  21874  evth2  21875  lebnumlem2  21877  reparphti  21912  pcoass  21939  pi1xfrcnv  21972  ipcau2  22092  minveclem4  22258  pjthlem1  22263  ovolunlem1a  22318  unmbl  22359  uniioombl  22415  iblitg  22594  dfitg  22595  itg0  22605  iblcnlem1  22613  itgcnlem  22615  itgabs  22660  limcdif  22699  limccnp  22714  limccnp2  22715  dvexp  22775  dvmptid  22779  dvmptc  22780  dvmptfsum  22795  dveflem  22799  dvsincos  22801  mvth  22812  dvlipcn  22814  dvivthlem1  22828  dvfsumle  22841  dvfsumlem2  22847  itgsubst  22869  tdeglem4  22877  tdeglem2  22878  plypf1  23025  plymullem1  23027  coesub  23070  dgrmulc  23084  fta1lem  23119  vieta1lem1  23122  vieta1lem2  23123  aalioulem4  23147  aaliou3lem3  23156  abelthlem2  23243  abelthlem8  23250  abelthlem9  23251  sinhalfpilem  23274  efhalfpi  23282  cospi  23283  efipi  23284  sin2pi  23286  cos2pi  23287  ef2pi  23288  sin2pim  23296  cos2pim  23297  sinmpi  23298  cosmpi  23299  sinppi  23300  cosppi  23301  sincosq4sgn  23312  tangtx  23316  sincos4thpi  23324  sincos6thpi  23326  sincos3rdpi  23327  pige3  23328  abssinper  23329  efif1olem4  23350  efifo  23352  eff1o  23354  circgrp  23357  circsubm  23358  logneg  23393  logimul  23419  logneg2  23420  dvrelog  23438  logcnlem4  23446  dvlog  23452  dvlog2  23454  logtayl  23461  1cxp  23473  ecxp  23474  cxpsqrt  23504  dvsqrt  23538  dvcnsqrt  23540  root1eq1  23551  cxpeq  23553  elogb  23563  ang180lem1  23594  ang180lem2  23595  heron  23620  1cubrlem  23623  1cubr  23624  dcubic2  23626  mcubic  23629  cubic2  23630  binom4  23632  dquartlem1  23633  dquartlem2  23634  dquart  23635  quart1lem  23637  quart1  23638  quartlem1  23639  asinsin  23674  asin1  23676  acos1  23677  atanlogsublem  23697  atanlogsub  23698  efiatan2  23699  2efiatan  23700  tanatan  23701  atanbnd  23708  atan1  23710  dvatan  23717  atantayl2  23720  leibpilem2  23723  leibpi  23724  log2cnv  23726  log2tlbnd  23727  log2ublem1  23728  log2ublem2  23729  log2ublem3  23730  log2ub  23731  birthday  23736  amgmlem  23771  emcllem5  23781  lgamgulmlem2  23811  lgamgulmlem5  23814  lgam1  23845  wilthlem2  23850  ftalem6  23858  basellem2  23862  basellem3  23863  basellem5  23865  basellem8  23868  cht1  23946  chp1  23948  1sgmprm  23981  ppiublem2  23985  ppiub  23986  chtublem  23993  chtub  23994  logfacbnd3  24005  bcp1ctr  24061  bclbnd  24062  bposlem1  24066  bposlem4  24069  bposlem6  24071  bposlem8  24073  bposlem9  24074  lgslem1  24078  lgsdir2lem1  24105  lgsdir2lem2  24106  lgsdir2lem3  24107  lgsdir2lem5  24109  lgs1  24120  lgseisenlem1  24131  lgseisenlem3  24133  lgsquadlem1  24136  lgsquadlem2  24137  lgsquad2lem2  24141  m1lgs  24144  2sqlem8  24154  2sqblem  24159  logdivsum  24225  mulog2sumlem2  24227  log2sumbnd  24236  selberglem1  24237  selberglem2  24238  pntrmax  24256  pntibndlem2  24283  pntibndlem3  24284  pntlemg  24290  pntlemr  24294  pntlemo  24299  ostth2lem3  24327  ostth2lem4  24328  istrkg3ld  24363  trgcgrg  24413  colperpexlem1  24620  ax5seglem7  24802  axlowdimlem4  24812  axlowdimlem16  24824  0wlk  25111  0trl  25112  wlkntrllem2  25126  wlkntrl  25128  constr1trl  25154  1pthonlem1  25155  constr2wlk  25164  constr2trl  25165  wlkdvspthlem  25173  constr3trllem3  25216  constr3trllem4  25217  constr3trllem5  25218  constr3pthlem1  25219  constr3pthlem3  25221  clwwlkn2  25339  clwlkisclwwlk2  25354  wwlkext2clwwlk  25367  vdgr1c  25469  nbhashuvtx1  25479  vdegp1ai  25548  vdegp1bi  25549  vdegp1ci  25550  extwwlkfablem2  25642  numclwwlkovf2ex  25650  numclwlk2lem2f  25667  frgraregord013  25682  ex-ind-dvds  25735  smcnlem  26169  ipidsq  26185  dipcj  26189  dip0r  26192  nmlnoubi  26273  nmblolbii  26276  blocnilem  26281  ip1ilem  26303  ip2i  26305  ipdirilem  26306  ipasslem10  26316  ipasslem11  26317  siilem1  26328  hvmul0  26503  hvsubsub4i  26538  hvnegdii  26541  hvsubeq0i  26542  hvsubcan2i  26543  hvsubaddi  26545  hvsub0  26555  hisubcomi  26583  normlem0  26588  normlem1  26589  normlem2  26590  normlem3  26591  normlem9  26597  norm-ii-i  26616  norm3difi  26626  normpari  26633  polid2i  26636  polidi  26637  bcsiALT  26658  pjhthlem1  26870  chdmm3i  26958  chdmm4i  26959  chjidm  26999  chj4i  27002  chjjdiri  27003  spanunsni  27058  pjoml4i  27066  cmcm2i  27072  qlax4i  27109  qlax5i  27110  pjadjii  27153  pjmulii  27156  pjsubii  27157  pjssmii  27160  pjcji  27163  pjneli  27202  hoadd32i  27257  ho0subi  27274  hosubid1  27277  hosd2i  27302  hopncani  27303  hosubeq0i  27305  lnopeq0lem1  27484  lnopunilem1  27489  lnophmlem2  27496  nmbdoplbi  27503  nmcopexi  27506  lnfnmuli  27523  nmcfnexi  27530  nmoptri2i  27578  nmopcoadji  27580  golem1  27750  mdsl1i  27800  cvmdi  27803  mdslmd3i  27811  csmdsymi  27813  xrge00  28276  archirngz  28335  archiabllem2c  28341  gsumle  28371  gsummpt2co  28372  gsumvsca1  28375  gsumvsca2  28376  xrge0slmod  28437  psgnfzto1st  28448  lmat22det  28478  madjusmdetlem4  28486  raddcn  28565  xrge0iifhom  28573  xrge0mulc1cn  28577  cbvesum  28693  gsumesum  28710  esumpfinvallem  28725  esumpfinvalf  28727  dya2icoseg  28929  sitg0  28998  eulerpartlemd  29016  eulerpartlemgvv  29026  eulerpartlemgh  29028  fib0  29049  fib1  29050  fibp1  29051  orrvcval4  29114  orrvcoel  29115  orrvccel  29116  coinflipprob  29129  coinflippvt  29134  ballotlem2  29138  ballotth  29187  signstf0  29236  signstfvn  29237  signsvtn0  29238  signstfvp  29239  signstfveq0  29245  signsvf0  29248  signsvf1  29249  signsvfn  29250  signshf  29256  subfacp1lem1  29681  subfacp1lem5  29686  subfacval2  29689  subfaclim  29690  subfacval3  29691  cvxpcon  29744  cvxscon  29745  mrsub0  29933  problem4  30079  quad3  30081  sinccvglem  30095  iexpire  30149  faclimlem1  30157  frrlem5  30296  fwddifnp1  30708  ptrest  31633  poimirlem25  31659  poimirlem27  31661  dvtan  31686  itgabsnc  31705  ftc1anclem8  31718  dvasin  31722  dvacos  31723  areacirclem1  31726  areacirclem4  31729  areacirc  31731  prdstotbnd  31820  prdsbnd2  31821  repwsmet  31860  rrnequiv  31861  reheibor  31865  dalem-cly  32935  pmodN  33114  cdleme0cp  33479  cdleme0cq  33480  cdleme1  33492  cdleme3d  33496  cdleme3h  33500  cdleme4  33503  cdleme5  33505  cdleme7a  33508  cdleme8  33515  cdleme9  33518  cdleme10  33519  cdleme11g  33530  cdleme15b  33540  cdleme21  33603  cdleme22e  33610  cdleme22eALTN  33611  cdleme23c  33617  cdleme25cv  33624  cdleme35b  33716  cdleme35c  33717  cdleme42a  33737  cdleme42d  33739  cdleme43aN  33755  cdlemeg46gfv  33796  cdlemk35  34178  dihjatcclem1  34685  lcdval2  34857  mapdpglem21  34959  mapfzcons  35257  mapfzcons1cl  35259  2rexfrabdioph  35338  3rexfrabdioph  35339  4rexfrabdioph  35340  6rexfrabdioph  35341  7rexfrabdioph  35342  rabdiophlem2  35344  diophren  35355  rabren3dioph  35357  pellexlem5  35377  pell1qr1  35415  rmspecfund  35453  jm2.17a  35506  jm2.17b  35507  jm2.27c  35558  jm2.27dlem5  35564  lmhmlnmsplit  35641  arearect  35789  areaquad  35790  relexp2  35898  trclfvdecomr  35949  inductionexd  36220  unitadd  36269  amgm2d  36277  amgm3d  36278  lhe4.4ex1a  36305  expgrowthi  36309  expgrowth  36311  bccn1  36320  binomcxplemdvbinom  36329  binomcxplemdvsum  36331  binomcxplemnotnn0  36332  binomcxp  36333  refsumcn  36981  oddfl  37086  m1expevenOLD  37232  sumnnodd  37272  cosnegpi  37304  dvcosre  37343  dvsinax  37345  ioodvbdlimc1lem2  37366  ioodvbdlimc2lem  37368  dvmptmulf  37371  dvxpaek  37374  dvmptfprod  37379  dvnprodlem2  37381  dvnprodlem3  37382  itgsin0pilem1  37385  itgsinexplem1  37389  itgsubsticclem  37411  stoweidlem13  37432  wallispilem4  37489  wallispi2lem1  37492  wallispi2lem2  37493  stirlinglem1  37495  dirkerper  37517  dirkertrigeqlem1  37519  dirkertrigeqlem3  37521  dirkertrigeq  37522  dirkeritg  37523  dirkercncflem1  37524  dirkercncflem2  37525  fourierdlem36  37564  fourierdlem41  37569  fourierdlem42  37570  fourierdlem48  37576  fourierdlem56  37584  fourierdlem57  37585  fourierdlem58  37586  fourierdlem60  37588  fourierdlem61  37589  fourierdlem62  37590  fourierdlem65  37593  fourierdlem73  37601  fourierdlem80  37608  fourierdlem87  37615  fourierdlem89  37617  fourierdlem90  37618  fourierdlem91  37619  fourierdlem100  37628  fourierdlem103  37631  fourierdlem107  37635  fourierdlem112  37640  fourierdlem113  37641  fourierdlem115  37643  fouriercnp  37648  sqwvfoura  37650  sqwvfourb  37651  fourierswlem  37652  fouriersw  37653  etransclem2  37658  etransclem37  37693  etransclem46  37702  1t10e1p1e11  38090  deccarry  38095  bits0ALTV  38188  nnsum3primes4  38263  nnsum3primesgbe  38267  nnsum4primesodd  38271  nnsum4primesoddALTV  38272  nnsum4primeseven  38275  nnsum4primesevenALTV  38276  bgoldbtbndlem1  38280  tgoldbachlt  38289  5tcu2e40  38295  3exp4mod41  38296  41prothprmlem1  38297  41prothprmlem2  38298  41prothprm  38299  pfx1  38332  pfxccatpfx1  38348  pfxccatpfx2  38349  uhgrepe  38438  2t6m3t4e0  38879  zlmodzxzequa  39039  zlmodzxznm  39040  zlmodzxzequap  39042  nn0sumshdiglemA  39181  nn0sumshdiglemB  39182  nn0sumshdiglem1  39183  sec0  39231
  Copyright terms: Public domain W3C validator