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

Theorem oveq2i 6616
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 6613 . 2 (𝐴 = 𝐵 → (𝐶𝐹𝐴) = (𝐶𝐹𝐵))
31, 2ax-mp 5 1 (𝐶𝐹𝐴) = (𝐶𝐹𝐵)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1480  (class class class)co 6605
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1841  ax-6 1890  ax-7 1937  ax-9 2001  ax-10 2021  ax-11 2036  ax-12 2049  ax-13 2250  ax-ext 2606
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1883  df-clab 2613  df-cleq 2619  df-clel 2622  df-nfc 2756  df-rex 2918  df-rab 2921  df-v 3193  df-dif 3563  df-un 3565  df-in 3567  df-ss 3574  df-nul 3897  df-if 4064  df-sn 4154  df-pr 4156  df-op 4160  df-uni 4408  df-br 4619  df-iota 5813  df-fv 5858  df-ov 6608
This theorem is referenced by:  caov32  6815  caov4  6819  caov42  6821  seqomsuc  7498  oa1suc  7557  o2p2e4  7567  om1  7568  oe1  7570  oawordeulem  7580  oeoalem  7622  nnm1  7674  nnm2  7675  nneob  7678  omopthlem1  7681  mapsnconst  7848  mapsncnv  7849  map2xp  8075  cantnflt  8514  cnfcom2  8544  infxpenc  8786  infxpenc2  8790  ackbij1lem5  8991  alephom  9352  pwxpndom2  9432  adderpqlem  9721  addassnq  9725  mulcanenq  9727  distrnq  9728  ltanq  9738  ltexnq  9742  halfnq  9743  ltrnq  9746  archnq  9747  addclprlem2  9784  prlem934  9800  prlem936  9814  addcmpblnr  9835  mulcmpblnrlem  9836  ltsrpr  9843  m1p1sr  9858  m1m1sr  9859  0idsr  9863  1idsr  9864  00sr  9865  pn0sr  9867  recexsrlem  9869  mulgt0sr  9871  sqgt0sr  9872  mulresr  9905  axmulcom  9921  axmulass  9923  axdistr  9924  axi2m1  9925  ax1rid  9927  axcnre  9930  mul02lem1  10157  addid1  10161  negid  10273  negsub  10274  subneg  10275  negsubdii  10311  muleqadd  10616  crne0  10958  2p2e4  11089  3p2e5  11105  3p3e6  11106  4p2e6  11107  4p3e7  11108  4p4e8  11109  5p2e7  11110  5p3e8  11111  5p4e9  11112  5p5e10OLD  11113  6p2e8  11114  6p3e9  11115  6p4e10OLD  11116  7p2e9  11117  7p3e10OLD  11118  8p2e10OLD  11119  3t3e9  11125  8th4div3  11197  halfpm6th  11198  addltmul  11213  div4p1lem1div2  11232  nn0n0n1ge2  11303  nneo  11405  zeo  11407  numsuc  11455  numltc  11472  numsucc  11493  numma  11501  nummul1c  11506  decrmac  11521  decsubi  11527  decsubiOLD  11528  decmul1  11529  decmul10add  11537  decmul10addOLD  11538  6p5lem  11539  5p5e10  11540  6p4e10  11542  7p3e10  11547  8p2e10  11554  4t3lem  11575  9t11e99  11615  9t11e99OLD  11616  decbin2  11627  xmulmnf1  12046  fztp  12336  fzprval  12340  fztpval  12341  fzshftral  12366  fz0tp  12378  fz0to3un2pr  12379  fzo01  12488  fzo12sn  12489  fzo13pr  12490  fzo0to2pr  12491  fzo0to3tp  12492  fzo0to42pr  12493  fzo1to4tp  12494  quoremz  12591  quoremnn0ALT  12593  intfrac2  12594  intfracq  12595  sqval  12859  sqrecii  12883  sq4e2t8  12899  cu2  12900  i3  12903  i4  12904  binom2i  12911  binom3  12922  crreczi  12926  3dec  12987  sq10OLD  12988  3decOLD  12990  nn0opthlem1  12992  facp1  13002  faclbnd  13014  faclbnd2  13015  faclbnd4lem1  13017  faclbnd4lem4  13020  bcn1  13037  bcn2  13043  4bc3eq4  13052  4bc2eq6  13053  hashgadd  13103  hashxplem  13157  hashmap  13159  hashfun  13161  hashbclem  13171  fz1isolem  13180  ccatlid  13303  ccatrid  13304  ccats1val2  13337  ccat2s1p2  13339  wrdeqs1cat  13407  swrdccatin12lem3  13422  swrdccat3a  13426  cats1fvn  13535  cats1cat  13538  cats2cat  13539  s3fn  13587  swrds2  13614  reim0  13787  cji  13828  sqrtm1  13945  absi  13955  rddif  14009  iseraltlem2  14342  iseralt  14344  fsump1i  14423  fsummulc2  14439  incexclem  14488  incexc  14489  arisum2  14513  geoihalfsum  14534  mertenslem1  14536  mertens  14538  risefall0lem  14677  risefac1  14684  fallfac1  14685  fallfacfwd  14687  bpoly0  14701  bpoly1  14702  bpolydiflem  14705  bpoly2  14708  bpoly3  14709  bpoly4  14710  fsumcube  14711  ef0lem  14729  ege2le3  14740  eft0val  14762  ef4p  14763  efgt1p2  14764  efgt1p  14765  tanval2  14783  efival  14802  ef01bndlem  14834  sin01bnd  14835  cos01bnd  14836  cos1bnd  14837  cos2bnd  14838  rpnnen2lem11  14873  sqr2irrlem  14897  3dvdsdec  14973  3dvdsdecOLD  14974  3dvds2dec  14975  3dvds2decOLD  14976  odd2np1lem  14983  odd2np1  14984  oddp1even  14987  opoe  15006  divalglem5  15039  divalglem6  15040  bits0  15069  0bits  15080  gcdaddmlem  15164  6gcd4e2  15174  lcmneg  15235  3lcm2e6woprm  15247  6lcm4e12  15248  3prm  15325  3lcm2e6  15359  phiprm  15401  eulerthlem2  15406  prmdiv  15409  pythagtriplem12  15450  pythagtriplem14  15452  pcmpt  15515  pcfac  15522  prmpwdvds  15527  pockthi  15530  prmreclem2  15540  prmreclem6  15544  4sqlem5  15565  4sqlem13  15580  modxai  15691  mod2xnegi  15694  gcdi  15696  decexp2  15698  numexpp1  15701  numexp2x  15702  decsplit0b  15703  decsplit1  15705  decsplit  15706  decsplit0bOLD  15707  decsplit1OLD  15709  decsplitOLD  15710  2exp16  15716  prmlem0  15731  139prm  15750  163prm  15751  317prm  15752  631prm  15753  1259lem4  15760  1259lem5  15761  1259prm  15762  2503lem1  15763  2503lem2  15764  2503lem3  15765  2503prm  15766  4001lem1  15767  4001lem4  15770  ressinbas  15852  rcaninv  16370  rescfth  16513  xpccatid  16744  oduval  17046  oppgmnd  17700  psgnunilem2  17831  psgnunilem4  17833  psgnpmtr  17846  psgn0fv0  17847  psgnsn  17856  psgnprfval1  17858  lsmmod2  18005  efgi0  18049  efgi1  18050  efginvrel2  18056  efgsval2  18062  efgsp1  18066  efgredleme  18072  efgredlemc  18074  efgcpbllemb  18084  frgpnabllem1  18192  lt6abl  18212  gsumconstf  18251  gsum2dlem2  18286  pwsgsum  18294  fsfnn0gsumfsffz  18295  dprd0  18346  dprdf1  18348  dprd2da  18357  ablfac1lem  18383  pgpfac1lem3  18392  pgpfaclem1  18396  srgbinomlem4  18459  opprring  18547  mulgass3  18553  evlsval  19433  mpff  19447  ply1assa  19483  gsumply1subr  19518  ply1coe  19580  coe1fzgsumdlem  19585  coe1fzgsumd  19586  gsumply1eq  19589  evl1gsumdlem  19634  evl1gsumd  19635  xrsnsgrp  19696  znbas  19806  znzrh2  19808  dsmmval2  19994  frlmip  20031  matgsum  20157  madetsumid  20181  mdetrsca  20323  mdetrsca2  20324  mdettpos  20331  m2detleiblem2  20348  madugsum  20363  madurid  20364  cpmat  20428  pmatcollpwfi  20501  pmatcollpw3fi1lem1  20505  pm2mpval  20514  mp2pm2mplem5  20529  chpmat1dlem  20554  chpmat1d  20555  chpidmat  20566  cpmidpmat  20592  cpmadugsumfi  20596  chcoeffeqlem  20604  cayleyhamilton0  20608  cayleyhamiltonALT  20610  cayleyhamilton1  20611  restin  20875  imacmp  21105  conncompconn  21140  uptx  21333  cnpflf2  21709  tmdgsum2  21805  tsmsres  21852  tsmsf1o  21853  tsmsmhm  21854  prdsxmet  22079  resspwsds  22082  prdsxmslem2  22239  tngngpim  22368  metdcn2  22545  metdcn  22546  metdscn2  22563  iimulcn  22640  icchmeo  22643  xrhmeo  22648  cnrehmeo  22655  cnheiborlem  22656  evth  22661  evth2  22662  lebnumlem2  22664  reparphti  22700  pcoass  22727  pi1xfrcnv  22760  ipcau2  22936  minveclem4  23106  pjthlem1  23111  ovolunlem1a  23166  unmbl  23207  uniioombl  23258  iblitg  23436  dfitg  23437  itg0  23447  iblcnlem1  23455  itgcnlem  23457  itgabs  23502  limcdif  23541  limccnp  23556  limccnp2  23557  dvexp  23617  dvmptid  23621  dvmptc  23622  dvmptfsum  23637  dveflem  23641  dvsincos  23643  mvth  23654  dvlipcn  23656  dvivthlem1  23670  dvfsumle  23683  dvfsumlem2  23689  itgsubst  23711  tdeglem4  23719  tdeglem2  23720  plypf1  23867  plymullem1  23869  coesub  23912  dgrmulc  23926  fta1lem  23961  vieta1lem1  23964  vieta1lem2  23965  aalioulem4  23989  aaliou3lem3  23998  abelthlem2  24085  abelthlem8  24092  abelthlem9  24093  sinhalfpilem  24114  efhalfpi  24122  cospi  24123  efipi  24124  sin2pi  24126  cos2pi  24127  ef2pi  24128  sin2pim  24136  cos2pim  24137  sinmpi  24138  cosmpi  24139  sinppi  24140  cosppi  24141  sincosq4sgn  24152  tangtx  24156  sincos4thpi  24164  sincos6thpi  24166  sincos3rdpi  24167  pige3  24168  abssinper  24169  efif1olem4  24190  efifo  24192  eff1o  24194  circgrp  24197  circsubm  24198  logneg  24233  logimul  24259  logneg2  24260  dvrelog  24278  logcnlem4  24286  dvlog  24292  dvlog2  24294  logtayl  24301  1cxp  24313  ecxp  24314  cxpsqrt  24344  dvsqrt  24378  dvcnsqrt  24380  root1eq1  24391  cxpeq  24393  elogb  24403  ang180lem1  24434  ang180lem2  24435  heron  24460  1cubrlem  24463  1cubr  24464  dcubic2  24466  mcubic  24469  cubic2  24470  binom4  24472  dquartlem1  24473  dquartlem2  24474  dquart  24475  quart1lem  24477  quart1  24478  quartlem1  24479  asinsin  24514  asin1  24516  acos1  24517  atanlogsublem  24537  atanlogsub  24538  efiatan2  24539  2efiatan  24540  tanatan  24541  atanbnd  24548  atan1  24550  dvatan  24557  atantayl2  24560  leibpilem2  24563  leibpi  24564  log2cnv  24566  log2tlbnd  24567  log2ublem1  24568  log2ublem2  24569  log2ublem3  24570  log2ub  24571  birthday  24576  amgmlem  24611  emcllem5  24621  lgamgulmlem2  24651  lgamgulmlem5  24654  lgam1  24685  wilthlem2  24690  ftalem6  24699  basellem2  24703  basellem3  24704  basellem5  24706  basellem8  24709  cht1  24786  chp1  24788  1sgmprm  24819  ppiublem2  24823  ppiub  24824  chtublem  24831  chtub  24832  logfacbnd3  24843  bcp1ctr  24899  bclbnd  24900  bposlem1  24904  bposlem4  24907  bposlem6  24909  bposlem8  24911  bposlem9  24912  lgslem1  24917  lgsdir2lem1  24945  lgsdir2lem2  24946  lgsdir2lem3  24947  lgsdir2lem5  24949  lgs1  24961  gausslemma2dlem1a  24985  gausslemma2dlem3  24988  gausslemma2dlem4  24989  gausslemma2d  24994  lgseisenlem1  24995  lgseisenlem3  24997  lgsquadlem1  25000  lgsquadlem2  25001  lgsquad2lem2  25005  m1lgs  25008  2lgslem1a2  25010  2sqlem8  25046  2sqblem  25051  logdivsum  25117  mulog2sumlem2  25119  log2sumbnd  25128  selberglem1  25129  selberglem2  25130  pntrmax  25148  pntibndlem2  25175  pntibndlem3  25176  pntlemg  25182  pntlemr  25186  pntlemo  25191  ostth2lem3  25219  ostth2lem4  25220  istrkg3ld  25255  trgcgrg  25305  tgcgr4  25321  colperpexlem1  25517  ax5seglem7  25710  axlowdimlem4  25720  axlowdimlem16  25732  setsiedg  25823  vdegp1ci  26314  wlkp1lem6  26438  wlkp1lem8  26440  wlkp1  26441  uhgrwkspthlem2  26513  pthdlem1  26525  pthdlem2  26527  pthd  26528  crctcshwlkn0lem4  26568  crctcshwlkn0lem5  26569  crctcshwlkn0lem6  26570  crctcshlem4  26575  crctcshwlkn0  26576  2wlkdlem2  26685  2wlkdlem4  26687  2pthdlem1  26689  clwlkclwwlk2  26765  wwlksext2clwwlk  26784  0ewlk  26835  1ewlk  26836  0wlk  26837  1pthdlem1  26855  1pthdlem2  26856  1wlkdlem1  26857  1wlkdlem4  26860  wlk2v2e  26877  3wlkdlem2  26880  3wlkdlem4  26882  3pthdlem1  26884  eupth0  26934  eupthp1  26936  eucrctshift  26963  eucrct2eupth  26965  extwwlkfablem1  27060  extwwlkfablem2  27062  numclwwlkovf2ex  27069  numclwlk2lem2f  27085  frgrregord013  27101  ex-exp  27155  ex-bc  27157  ex-gcd  27162  ex-lcm  27163  ex-ind-dvds  27166  smcnlem  27392  ipidsq  27405  dipcj  27409  dip0r  27412  nmlnoubi  27491  nmblolbii  27494  blocnilem  27499  ip1ilem  27521  ip2i  27523  ipdirilem  27524  ipasslem10  27534  ipasslem11  27535  siilem1  27546  hvmul0  27721  hvsubsub4i  27756  hvnegdii  27759  hvsubeq0i  27760  hvsubcan2i  27761  hvsubaddi  27763  hvsub0  27773  hisubcomi  27801  normlem0  27806  normlem1  27807  normlem2  27808  normlem3  27809  normlem9  27815  norm-ii-i  27834  norm3difi  27844  normpari  27851  polid2i  27854  polidi  27855  bcsiALT  27876  pjhthlem1  28090  chdmm3i  28178  chdmm4i  28179  chjidm  28219  chj4i  28222  chjjdiri  28223  spanunsni  28278  pjoml4i  28286  cmcm2i  28292  qlax4i  28329  qlax5i  28330  pjadjii  28373  pjmulii  28376  pjsubii  28377  pjssmii  28380  pjcji  28383  pjneli  28422  hoadd32i  28477  ho0subi  28494  hosubid1  28497  hosd2i  28522  hopncani  28523  hosubeq0i  28525  lnopeq0lem1  28704  lnopunilem1  28709  lnophmlem2  28716  nmbdoplbi  28723  nmcopexi  28726  lnfnmuli  28743  nmcfnexi  28750  nmoptri2i  28798  nmopcoadji  28800  golem1  28970  mdsl1i  29020  cvmdi  29023  mdslmd3i  29031  csmdsymi  29033  xrge00  29463  archirngz  29520  archiabllem2c  29526  gsumle  29556  gsummpt2co  29557  gsumvsca1  29559  gsumvsca2  29560  xrge0slmod  29621  psgnfzto1st  29632  lmat22det  29662  madjusmdetlem4  29670  raddcn  29749  xrge0iifhom  29757  xrge0mulc1cn  29761  cbvesum  29877  gsumesum  29894  esumpfinvallem  29909  esumpfinvalf  29911  dya2icoseg  30112  sitg0  30181  eulerpartlemd  30201  eulerpartlemgvv  30211  eulerpartlemgh  30213  fib0  30234  fib1  30235  fibp1  30236  orrvcval4  30299  orrvcoel  30300  orrvccel  30301  coinflipprob  30314  coinflippvt  30319  ballotlem2  30323  ballotth  30372  signstf0  30417  signstfvn  30418  signsvtn0  30419  signstfvp  30420  signstfveq0  30426  signsvf0  30429  signsvf1  30430  signsvfn  30431  signshf  30437  subfacp1lem1  30861  subfacp1lem5  30866  subfacval2  30869  subfaclim  30870  subfacval3  30871  cvxpconn  30924  cvxsconn  30925  mrsub0  31113  problem4  31262  quad3  31264  sinccvglem  31266  iexpire  31320  faclimlem1  31328  frrlem5  31473  fwddifnp1  31887  knoppcnlem10  32107  knoppndvlem7  32124  knoppndvlem21  32138  cnndvlem1  32143  finxpreclem4  32836  ptrest  33007  poimirlem27  33035  dvtan  33059  itgabsnc  33078  ftc1anclem8  33091  dvasin  33095  dvacos  33096  areacirclem1  33099  areacirclem4  33102  areacirc  33104  prdstotbnd  33192  prdsbnd2  33193  repwsmet  33232  rrnequiv  33233  reheibor  33237  dalem-cly  34404  pmodN  34583  cdleme0cp  34948  cdleme0cq  34949  cdleme1  34961  cdleme3d  34965  cdleme3h  34969  cdleme4  34972  cdleme5  34974  cdleme7a  34977  cdleme8  34984  cdleme9  34987  cdleme10  34988  cdleme11g  34999  cdleme15b  35009  cdleme21  35072  cdleme22e  35079  cdleme22eALTN  35080  cdleme23c  35086  cdleme25cv  35093  cdleme35b  35185  cdleme35c  35186  cdleme42a  35206  cdleme42d  35208  cdleme43aN  35224  cdlemeg46gfv  35265  cdlemk35  35647  dihjatcclem1  36154  lcdval2  36326  mapdpglem21  36428  mapfzcons  36726  mapfzcons1cl  36728  2rexfrabdioph  36807  3rexfrabdioph  36808  4rexfrabdioph  36809  6rexfrabdioph  36810  7rexfrabdioph  36811  rabdiophlem2  36813  diophren  36824  rabren3dioph  36826  pellexlem5  36844  pell1qr1  36882  rmspecfund  36921  jm2.17a  36974  jm2.17b  36975  jm2.27c  37021  jm2.27dlem5  37027  lmhmlnmsplit  37104  arearect  37249  areaquad  37250  relexp2  37417  trclfvdecomr  37468  k0004val0  37901  inductionexd  37902  unitadd  37947  amgm2d  37950  amgm3d  37951  lhe4.4ex1a  37977  expgrowthi  37981  expgrowth  37983  bccn1  37992  binomcxplemdvbinom  38001  binomcxplemdvsum  38003  binomcxplemnotnn0  38004  binomcxp  38005  refsumcn  38639  unirnmapsn  38847  oddfl  38921  infleinflem2  39019  sumnnodd  39234  cosnegpi  39349  dvcosre  39398  dvsinax  39400  ioodvbdlimc1lem2  39421  ioodvbdlimc2lem  39423  dvmptmulf  39426  dvxpaek  39429  dvmptfprod  39434  dvnprodlem2  39436  dvnprodlem3  39437  itgsin0pilem1  39440  itgsinexplem1  39444  itgsubsticclem  39466  stoweidlem13  39505  wallispilem4  39560  wallispi2lem1  39563  wallispi2lem2  39564  stirlinglem1  39566  dirkerper  39588  dirkertrigeqlem1  39590  dirkertrigeqlem3  39592  dirkertrigeq  39593  dirkeritg  39594  dirkercncflem1  39595  dirkercncflem2  39596  fourierdlem36  39635  fourierdlem41  39640  fourierdlem42  39641  fourierdlem48  39646  fourierdlem56  39654  fourierdlem57  39655  fourierdlem58  39656  fourierdlem60  39658  fourierdlem61  39659  fourierdlem62  39660  fourierdlem65  39663  fourierdlem73  39671  fourierdlem80  39678  fourierdlem87  39685  fourierdlem89  39687  fourierdlem90  39688  fourierdlem91  39689  fourierdlem100  39698  fourierdlem103  39701  fourierdlem107  39705  fourierdlem112  39710  fourierdlem113  39711  fourierdlem115  39713  fouriercnp  39718  sqwvfoura  39720  sqwvfourb  39721  fourierswlem  39722  fouriersw  39723  etransclem2  39728  etransclem37  39763  etransclem46  39772  hoidmvlelem3  40086  vonioolem2  40170  issmflem  40211  smfmullem2  40274  1t10e1p1e11  40585  1t10e1p1e11OLD  40586  pfx1  40679  pfxccatpfx1  40695  pfxccatpfx2  40696  fmtno0  40720  fmtno1  40721  fmtnorec2lem  40722  fmtnorec3  40728  fmtno2  40730  fmtno3  40731  fmtno4  40732  fmtno4sqrt  40751  fmtno4prmfac  40752  2exp5  40775  139prmALT  40779  31prm  40780  2exp7  40782  2exp11  40785  mod42tp1mod8  40787  lighneallem2  40791  5tcu2e40  40800  3exp4mod41  40801  41prothprmlem1  40802  41prothprmlem2  40803  41prothprm  40804  bits0ALTV  40858  nnsum3primes4  40934  nnsum3primesgbe  40938  nnsum4primesodd  40942  nnsum4primesoddALTV  40943  nnsum4primeseven  40946  nnsum4primesevenALTV  40947  bgoldbtbndlem1  40951  tgoldbachlt  40960  tgoldbachltOLD  40967  2t6m3t4e0  41368  zlmodzxzequa  41528  zlmodzxznm  41529  zlmodzxzequap  41531  nn0sumshdiglemA  41660  nn0sumshdiglemB  41661  nn0sumshdiglem1  41662  sec0  41749  dfdp2OLD  41756  amgmw2d  41808
  Copyright terms: Public domain W3C validator