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

Theorem oveq2i 6806
Description: Equality inference for operation value. (Contributed by NM, 28-Feb-1995.)
Hypothesis
Ref Expression
oveq1i.1 𝐴 = 𝐵
Assertion
Ref Expression
oveq2i (𝐶𝐹𝐴) = (𝐶𝐹𝐵)

Proof of Theorem oveq2i
StepHypRef Expression
1 oveq1i.1 . 2 𝐴 = 𝐵
2 oveq2 6803 . 2 (𝐴 = 𝐵 → (𝐶𝐹𝐴) = (𝐶𝐹𝐵))
31, 2ax-mp 5 1 (𝐶𝐹𝐴) = (𝐶𝐹𝐵)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1631  (class class class)co 6795
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-rex 3067  df-rab 3070  df-v 3353  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-nul 4064  df-if 4227  df-sn 4318  df-pr 4320  df-op 4324  df-uni 4576  df-br 4788  df-iota 5993  df-fv 6038  df-ov 6798
This theorem is referenced by:  caov32  7011  caov4  7015  caov42  7017  seqomsuc  7708  oa1suc  7768  o2p2e4  7778  om1  7779  oe1  7781  oawordeulem  7791  oeoalem  7833  nnm1  7885  nnm2  7886  nneob  7889  omopthlem1  7892  mapsnconst  8060  mapsncnv  8061  map2xp  8289  cantnflt  8736  cnfcom2  8766  infxpenc  9044  infxpenc2  9048  ackbij1lem5  9251  alephom  9612  pwxpndom2  9692  adderpqlem  9981  addassnq  9985  mulcanenq  9987  distrnq  9988  ltanq  9998  ltexnq  10002  halfnq  10003  ltrnq  10006  archnq  10007  addclprlem2  10044  prlem934  10060  prlem936  10074  addcmpblnr  10095  mulcmpblnrlem  10096  ltsrpr  10103  m1p1sr  10118  m1m1sr  10119  0idsr  10123  1idsr  10124  00sr  10125  pn0sr  10127  recexsrlem  10129  mulgt0sr  10131  sqgt0sr  10132  mulresr  10165  axmulcom  10181  axmulass  10183  axdistr  10184  axi2m1  10185  ax1rid  10187  axcnre  10190  mul02lem1  10417  addid1  10421  negid  10533  negsub  10534  subneg  10535  negsubdii  10571  muleqadd  10876  crne0  11218  2p2e4  11350  3p2e5  11366  3p3e6  11367  4p2e6  11368  4p3e7  11369  4p4e8  11370  5p2e7  11371  5p3e8  11372  5p4e9  11373  5p5e10OLD  11374  6p2e8  11375  6p3e9  11376  6p4e10OLD  11377  7p2e9  11378  7p3e10OLD  11379  8p2e10OLD  11380  3t3e9  11386  8th4div3  11458  halfpm6th  11459  addltmul  11474  div4p1lem1div2  11493  nn0n0n1ge2  11564  nneo  11667  zeo  11669  numsuc  11717  numltc  11734  numsucc  11755  numma  11762  nummul1c  11767  decrmac  11782  decsubi  11788  decsubiOLD  11789  decmul1  11790  decmul10add  11798  decmul10addOLD  11799  6p5lem  11800  5p5e10  11801  6p4e10  11803  7p3e10  11808  8p2e10  11815  4t3lem  11836  9t11e99  11876  9t11e99OLD  11877  decbin2  11888  xmulmnf1  12310  fztp  12603  fzprval  12607  fztpval  12608  fzshftral  12634  fz0tp  12647  fz0to3un2pr  12648  fzo01  12757  fzo12sn  12758  fzo13pr  12759  fzo0to2pr  12760  fzo0to3tp  12761  fzo0to42pr  12762  fzo1to4tp  12763  fzosplitprm1  12785  quoremz  12861  quoremnn0ALT  12863  intfrac2  12864  intfracq  12865  sqval  13128  sqrecii  13152  sq4e2t8  13168  cu2  13169  i3  13172  i4  13173  binom2i  13180  binom3  13191  crreczi  13195  3dec  13256  nn0opthlem1  13258  facp1  13268  faclbnd  13280  faclbnd2  13281  faclbnd4lem1  13283  faclbnd4lem4  13286  bcn1  13303  bcn2  13309  4bc3eq4  13318  4bc2eq6  13319  hashgadd  13367  hashxplem  13421  hashmap  13423  hashfun  13425  hashbclem  13437  fz1isolem  13446  ccatlid  13567  ccatrid  13568  ccats1val2  13609  ccat2s1p2  13612  wrdeqs1cat  13682  swrdccatin12lem3  13698  swrdccat3a  13702  cats1fvn  13811  cats1cat  13814  cats2cat  13815  s3fn  13864  swrds2  13893  swrds2m  13894  reim0  14065  cji  14106  sqrtm1  14223  absi  14233  rddif  14287  iseraltlem2  14620  iseralt  14622  fsump1i  14707  fsummulc2  14722  incexclem  14774  incexc  14775  arisum2  14799  geoihalfsum  14820  mertenslem1  14822  mertens  14824  risefall0lem  14962  risefac1  14969  fallfac1  14970  fallfacfwd  14972  bpoly0  14986  bpoly1  14987  bpolydiflem  14990  bpoly2  14993  bpoly3  14994  bpoly4  14995  fsumcube  14996  ef0lem  15014  ege2le3  15025  eft0val  15047  ef4p  15048  efgt1p2  15049  efgt1p  15050  tanval2  15068  efival  15087  ef01bndlem  15119  sin01bnd  15120  cos01bnd  15121  cos1bnd  15122  cos2bnd  15123  rpnnen2lem11  15158  sqrt2irrlemOLD  15183  3dvdsdec  15262  3dvdsdecOLD  15263  3dvds2dec  15264  odd2np1lem  15271  odd2np1  15272  oddp1even  15275  opoe  15294  divalglem5  15327  divalglem6  15328  bits0  15357  0bits  15368  gcdaddmlem  15452  6gcd4e2  15462  lcmneg  15523  3lcm2e6woprm  15535  6lcm4e12  15536  3prm  15612  3lcm2e6  15646  phiprm  15688  eulerthlem2  15693  prmdiv  15696  pythagtriplem12  15737  pythagtriplem14  15739  pcmpt  15802  pcfac  15809  prmpwdvds  15814  pockthi  15817  prmreclem2  15827  prmreclem6  15831  4sqlem5  15852  4sqlem13  15867  modxai  15978  mod2xnegi  15981  gcdi  15983  decexp2  15985  numexpp1  15988  numexp2x  15989  decsplit0b  15990  decsplit1  15992  decsplit  15993  decsplit0bOLD  15994  decsplit1OLD  15996  decsplitOLD  15997  2exp16  16003  prmlem0  16018  139prm  16037  163prm  16038  317prm  16039  631prm  16040  1259lem4  16047  1259lem5  16048  1259prm  16049  2503lem1  16050  2503lem2  16051  2503lem3  16052  2503prm  16053  4001lem1  16054  4001lem4  16057  ressinbas  16142  rcaninv  16660  rescfth  16803  xpccatid  17035  oduval  17337  oppgmnd  17990  psgnunilem2  18121  psgnunilem4  18123  psgnpmtr  18136  psgn0fv0  18137  psgnsn  18146  psgnprfval1  18148  lsmmod2  18295  efgi0  18339  efgi1  18340  efginvrel2  18346  efgsval2  18352  efgsp1  18356  efgredleme  18362  efgredlemc  18364  efgcpbllemb  18374  frgpnabllem1  18482  lt6abl  18502  gsumconstf  18541  gsum2dlem2  18576  pwsgsum  18584  fsfnn0gsumfsffz  18585  dprd0  18637  dprdf1  18639  dprd2da  18648  ablfac1lem  18674  pgpfac1lem3  18683  pgpfaclem1  18687  srgbinomlem4  18750  opprring  18838  mulgass3  18844  evlsval  19733  mpff  19747  ply1assa  19783  gsumply1subr  19818  ply1coe  19880  coe1fzgsumdlem  19885  coe1fzgsumd  19886  gsumply1eq  19889  evl1gsumdlem  19934  evl1gsumd  19935  xrsnsgrp  19996  znbas  20106  znzrh2  20108  dsmmval2  20296  frlmip  20333  matgsum  20459  madetsumid  20484  mdetrsca  20626  mdetrsca2  20627  mdettpos  20634  m2detleiblem2  20651  madugsum  20666  madurid  20667  cpmat  20733  pmatcollpwfi  20806  pmatcollpw3fi1lem1  20810  pm2mpval  20819  mp2pm2mplem5  20834  chpmat1dlem  20859  chpmat1d  20860  chpidmat  20871  cpmidpmat  20897  cpmadugsumfi  20901  chcoeffeqlem  20909  cayleyhamilton0  20913  cayleyhamiltonALT  20915  cayleyhamilton1  20916  restin  21190  imacmp  21420  conncompconn  21455  uptx  21648  cnpflf2  22023  tmdgsum2  22119  tsmsres  22166  tsmsf1o  22167  tsmsmhm  22168  prdsxmet  22393  resspwsds  22396  prdsxmslem2  22553  tngngpim  22682  metdcn2  22861  metdcn  22862  metdscn2  22879  iimulcn  22956  icchmeo  22959  xrhmeo  22964  cnrehmeo  22971  cnheiborlem  22972  evth  22977  evth2  22978  lebnumlem2  22980  reparphti  23015  pcoass  23042  pi1xfrcnv  23075  ipcau2  23251  minveclem4  23421  pjthlem1  23426  ovolunlem1a  23483  unmbl  23524  uniioombl  23576  iblitg  23754  dfitg  23755  itg0  23765  iblcnlem1  23773  itgcnlem  23775  itgabs  23820  limcdif  23859  limccnp  23874  limccnp2  23875  dvexp  23935  dvmptid  23939  dvmptc  23940  dvmptfsum  23957  dveflem  23961  dvsincos  23963  mvth  23974  dvlipcn  23976  dvivthlem1  23990  dvfsumle  24003  dvfsumlem2  24009  itgsubst  24031  tdeglem4  24039  tdeglem2  24040  plypf1  24187  plymullem1  24189  coesub  24232  dgrmulc  24246  fta1lem  24281  vieta1lem1  24284  vieta1lem2  24285  aalioulem4  24309  aaliou3lem3  24318  abelthlem2  24405  abelthlem8  24412  abelthlem9  24413  sinhalfpilem  24435  efhalfpi  24443  cospi  24444  efipi  24445  sin2pi  24447  cos2pi  24448  ef2pi  24449  sin2pim  24457  cos2pim  24458  sinmpi  24459  cosmpi  24460  sinppi  24461  cosppi  24462  sincosq4sgn  24473  tangtx  24477  sincos4thpi  24485  sincos6thpi  24487  sincos3rdpi  24488  pige3  24489  abssinper  24490  efif1olem4  24511  efifo  24513  eff1o  24515  circgrp  24518  circsubm  24519  logneg  24554  logimul  24580  logneg2  24581  dvrelog  24603  logcnlem4  24611  dvlog  24617  dvlog2  24619  logtayl  24626  1cxp  24638  ecxp  24639  cxpsqrt  24669  dvsqrt  24703  dvcnsqrt  24705  root1eq1  24716  cxpeq  24718  elogb  24728  ang180lem1  24759  ang180lem2  24760  heron  24785  1cubrlem  24788  1cubr  24789  dcubic2  24791  mcubic  24794  cubic2  24795  binom4  24797  dquartlem1  24798  dquartlem2  24799  dquart  24800  quart1lem  24802  quart1  24803  quartlem1  24804  asinsin  24839  asin1  24841  acos1  24842  atanlogsublem  24862  atanlogsub  24863  efiatan2  24864  2efiatan  24865  tanatan  24866  atanbnd  24873  atan1  24875  dvatan  24882  atantayl2  24885  leibpilem2  24888  leibpi  24889  log2cnv  24891  log2tlbnd  24892  log2ublem1  24893  log2ublem2  24894  log2ublem3  24895  log2ub  24896  birthday  24901  amgmlem  24936  emcllem5  24946  lgamgulmlem2  24976  lgamgulmlem5  24979  lgam1  25010  wilthlem2  25015  ftalem6  25024  basellem2  25028  basellem3  25029  basellem5  25031  basellem8  25034  cht1  25111  chp1  25113  1sgmprm  25144  ppiublem2  25148  ppiub  25149  chtublem  25156  chtub  25157  logfacbnd3  25168  bcp1ctr  25224  bclbnd  25225  bposlem1  25229  bposlem4  25232  bposlem6  25234  bposlem8  25236  bposlem9  25237  lgslem1  25242  lgsdir2lem1  25270  lgsdir2lem2  25271  lgsdir2lem3  25272  lgsdir2lem5  25274  lgs1  25286  gausslemma2dlem1a  25310  gausslemma2dlem3  25313  gausslemma2dlem4  25314  gausslemma2d  25319  lgseisenlem1  25320  lgseisenlem3  25322  lgsquadlem1  25325  lgsquadlem2  25326  lgsquad2lem2  25330  m1lgs  25333  2lgslem1a2  25335  2sqlem8  25371  2sqblem  25376  logdivsum  25442  mulog2sumlem2  25444  log2sumbnd  25453  selberglem1  25454  selberglem2  25455  pntrmax  25473  pntibndlem2  25500  pntibndlem3  25501  pntlemg  25507  pntlemr  25511  pntlemo  25516  ostth2lem3  25544  ostth2lem4  25545  istrkg3ld  25580  trgcgrg  25630  tgcgr4  25646  colperpexlem1  25842  ax5seglem7  26035  axlowdimlem4  26045  axlowdimlem16  26057  setsiedg  26148  vdegp1ci  26668  finsumvtxdg2sstep  26679  finsumvtxdg2size  26680  wlkp1lem6  26809  wlkp1lem8  26811  wlkp1  26812  uhgrwkspthlem2  26884  pthdlem1  26896  pthdlem2  26898  pthd  26899  crctcshwlkn0lem4  26940  crctcshwlkn0lem5  26941  crctcshwlkn0lem6  26942  crctcshlem4  26947  crctcshwlkn0  26948  2wlkdlem2  27072  2wlkdlem4  27074  2pthdlem1  27076  wwlks2onv  27099  clwlkclwwlk2  27152  wwlksext2clwwlk  27213  wwlksext2clwwlkOLD  27214  clwwlknonex2lem1  27282  0ewlk  27293  1ewlk  27294  0wlk  27295  1pthdlem1  27314  1pthdlem2  27315  1wlkdlem1  27316  1wlkdlem4  27319  wlk2v2e  27336  3wlkdlem2  27339  3wlkdlem4  27341  3pthdlem1  27343  eupth0  27393  eupthp1  27395  eucrctshift  27422  eucrct2eupth  27424  extwwlkfablem1OLD  27523  numclwwlk1lem2foalem  27536  numclwlk2lem2f  27567  numclwlk2lem2fOLD  27574  frgrregord013  27593  ex-exp  27648  ex-bc  27650  ex-gcd  27655  ex-lcm  27656  ex-ind-dvds  27659  smcnlem  27891  ipidsq  27904  dipcj  27908  dip0r  27911  nmlnoubi  27990  nmblolbii  27993  blocnilem  27998  ip1ilem  28020  ip2i  28022  ipdirilem  28023  ipasslem10  28033  ipasslem11  28034  siilem1  28045  hvmul0  28220  hvsubsub4i  28255  hvnegdii  28258  hvsubeq0i  28259  hvsubcan2i  28260  hvsubaddi  28262  hvsub0  28272  hisubcomi  28300  normlem0  28305  normlem1  28306  normlem2  28307  normlem3  28308  normlem9  28314  norm-ii-i  28333  norm3difi  28343  normpari  28350  polid2i  28353  polidi  28354  bcsiALT  28375  pjhthlem1  28589  chdmm3i  28677  chdmm4i  28678  chjidm  28718  chj4i  28721  chjjdiri  28722  spanunsni  28777  pjoml4i  28785  cmcm2i  28791  qlax4i  28828  qlax5i  28829  pjadjii  28872  pjmulii  28875  pjsubii  28876  pjssmii  28879  pjcji  28882  pjneli  28921  hoadd32i  28976  ho0subi  28993  hosubid1  28996  hosd2i  29021  hopncani  29022  hosubeq0i  29024  lnopeq0lem1  29203  lnopunilem1  29208  lnophmlem2  29215  nmbdoplbi  29222  nmcopexi  29225  lnfnmuli  29242  nmcfnexi  29249  nmoptri2i  29297  nmopcoadji  29299  golem1  29469  mdsl1i  29519  cvmdi  29522  mdslmd3i  29530  csmdsymi  29532  dfdec100  29915  dfdp2OLD  29918  dp20u  29924  dpmul10  29942  dpmul100  29944  dp3mul10  29945  dpmul1000  29946  dpexpp1  29955  0dp2dp  29956  dpmul  29960  dpmul4  29961  1mhdrd  29963  xrge00  30025  archirngz  30082  archiabllem2c  30088  gsumle  30118  gsummpt2co  30119  gsumvsca1  30121  gsumvsca2  30122  xrge0slmod  30183  psgnfzto1st  30194  lmat22det  30227  madjusmdetlem4  30235  raddcn  30314  xrge0iifhom  30322  xrge0mulc1cn  30326  cbvesum  30443  gsumesum  30460  esumpfinvallem  30475  esumpfinvalf  30477  dya2icoseg  30678  sitg0  30747  eulerpartlemd  30767  eulerpartlemgvv  30777  eulerpartlemgh  30779  fib0  30800  fib1  30801  fibp1  30802  orrvcval4  30865  orrvcoel  30866  orrvccel  30867  coinflipprob  30880  coinflippvt  30885  ballotlem2  30889  ballotth  30938  signstf0  30984  signstfvn  30985  signsvtn0  30986  signstfvp  30987  signstfveq0  30993  signsvf0  30996  signsvf1  30997  signsvfn  30998  signshf  31004  prodfzo03  31020  itgexpif  31023  repr0  31028  hgt750lemd  31065  hgt750lem  31068  hgt750lem2  31069  subfacp1lem1  31498  subfacp1lem5  31503  subfacval2  31506  subfaclim  31507  subfacval3  31508  cvxpconn  31561  cvxsconn  31562  mrsub0  31750  problem4  31899  quad3  31901  sinccvglem  31903  iexpire  31958  faclimlem1  31966  frrlem5  32120  fwddifnp1  32608  knoppcnlem10  32828  knoppndvlem7  32845  knoppndvlem21  32859  cnndvlem1  32864  finxpreclem4  33567  ptrest  33740  poimirlem27  33768  dvtan  33791  itgabsnc  33810  ftc1anclem8  33823  dvasin  33827  dvacos  33828  areacirclem1  33831  areacirclem4  33834  areacirc  33836  prdstotbnd  33924  prdsbnd2  33925  repwsmet  33964  rrnequiv  33965  reheibor  33969  dalem-cly  35479  pmodN  35658  cdleme0cp  36023  cdleme0cq  36024  cdleme1  36036  cdleme3d  36040  cdleme3h  36044  cdleme4  36047  cdleme5  36049  cdleme7a  36052  cdleme8  36059  cdleme9  36062  cdleme10  36063  cdleme11g  36074  cdleme15b  36084  cdleme21  36146  cdleme22e  36153  cdleme22eALTN  36154  cdleme23c  36160  cdleme25cv  36167  cdleme35b  36259  cdleme35c  36260  cdleme42a  36280  cdleme42d  36282  cdleme43aN  36298  cdlemeg46gfv  36339  cdlemk35  36721  dihjatcclem1  37228  lcdval2  37400  mapdpglem21  37502  mapfzcons  37805  mapfzcons1cl  37807  2rexfrabdioph  37886  3rexfrabdioph  37887  4rexfrabdioph  37888  6rexfrabdioph  37889  7rexfrabdioph  37890  rabdiophlem2  37892  diophren  37903  rabren3dioph  37905  pellexlem5  37923  pell1qr1  37961  rmspecfund  38000  jm2.17a  38053  jm2.17b  38054  jm2.27c  38100  jm2.27dlem5  38106  lmhmlnmsplit  38183  arearect  38327  areaquad  38328  relexp2  38495  trclfvdecomr  38546  k0004val0  38978  inductionexd  38979  unitadd  39024  amgm2d  39027  amgm3d  39028  lhe4.4ex1a  39054  expgrowthi  39058  expgrowth  39060  bccn1  39069  binomcxplemdvbinom  39078  binomcxplemdvsum  39080  binomcxplemnotnn0  39081  binomcxp  39082  refsumcn  39711  unirnmapsn  39923  oddfl  40004  infleinflem2  40100  sumnnodd  40377  cosnegpi  40593  dvcosre  40641  dvsinax  40642  ioodvbdlimc1lem2  40662  ioodvbdlimc2lem  40664  dvmptmulf  40667  dvxpaek  40670  dvmptfprod  40675  dvnprodlem2  40677  dvnprodlem3  40678  itgsin0pilem1  40680  itgsinexplem1  40684  itgsubsticclem  40705  stoweidlem13  40744  wallispilem4  40799  wallispi2lem1  40802  wallispi2lem2  40803  stirlinglem1  40805  dirkerper  40827  dirkertrigeqlem1  40829  dirkertrigeqlem3  40831  dirkertrigeq  40832  dirkeritg  40833  dirkercncflem1  40834  dirkercncflem2  40835  fourierdlem36  40874  fourierdlem41  40879  fourierdlem42  40880  fourierdlem48  40885  fourierdlem56  40893  fourierdlem57  40894  fourierdlem58  40895  fourierdlem60  40897  fourierdlem61  40898  fourierdlem62  40899  fourierdlem65  40902  fourierdlem73  40910  fourierdlem80  40917  fourierdlem87  40924  fourierdlem89  40926  fourierdlem90  40927  fourierdlem91  40928  fourierdlem100  40937  fourierdlem103  40940  fourierdlem107  40944  fourierdlem112  40949  fourierdlem113  40950  fourierdlem115  40952  fouriercnp  40957  sqwvfoura  40959  sqwvfourb  40960  fourierswlem  40961  fouriersw  40962  etransclem2  40967  etransclem37  41002  etransclem46  41011  hoidmvlelem3  41328  vonioolem2  41412  issmflem  41453  smfmullem2  41516  1t10e1p1e11  41844  1t10e1p1e11OLD  41845  pfx1  41936  pfxccatpfx1  41952  pfxccatpfx2  41953  fmtno0  41977  fmtno1  41978  fmtnorec2lem  41979  fmtnorec3  41985  fmtno2  41987  fmtno3  41988  fmtno4  41989  fmtno4sqrt  42008  fmtno4prmfac  42009  2exp5  42032  139prmALT  42036  31prm  42037  2exp7  42039  2exp11  42042  mod42tp1mod8  42044  lighneallem2  42048  5tcu2e40  42057  3exp4mod41  42058  41prothprmlem1  42059  41prothprmlem2  42060  41prothprm  42061  bits0ALTV  42115  sbgoldbo  42200  nnsum3primes4  42201  nnsum3primesgbe  42205  nnsum4primesodd  42209  nnsum4primesoddALTV  42210  nnsum4primeseven  42213  nnsum4primesevenALTV  42214  bgoldbtbndlem1  42218  tgoldbachlt  42229  tgoldbachltOLD  42235  2t6m3t4e0  42651  zlmodzxzequa  42810  zlmodzxznm  42811  zlmodzxzequap  42813  nn0sumshdiglemA  42938  nn0sumshdiglemB  42939  nn0sumshdiglem1  42940  sec0  43029  amgmw2d  43078
  Copyright terms: Public domain W3C validator