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

Theorem oveq2i 6538
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 6535 . 2 (𝐴 = 𝐵 → (𝐶𝐹𝐴) = (𝐶𝐹𝐵))
31, 2ax-mp 5 1 (𝐶𝐹𝐴) = (𝐶𝐹𝐵)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1474  (class class class)co 6527
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-rex 2901  df-rab 2904  df-v 3174  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-nul 3874  df-if 4036  df-sn 4125  df-pr 4127  df-op 4131  df-uni 4367  df-br 4578  df-iota 5754  df-fv 5798  df-ov 6530
This theorem is referenced by:  caov32  6736  caov4  6740  caov42  6742  seqomsuc  7416  oa1suc  7475  o2p2e4  7485  om1  7486  oe1  7488  oawordeulem  7498  oeoalem  7540  nnm1  7592  nnm2  7593  nneob  7596  omopthlem1  7599  mapsnconst  7766  mapsncnv  7767  map2xp  7992  cantnflt  8429  cnfcom2  8459  infxpenc  8701  infxpenc2  8705  ackbij1lem5  8906  alephom  9263  pwxpndom2  9343  adderpqlem  9632  addassnq  9636  mulcanenq  9638  distrnq  9639  ltanq  9649  ltexnq  9653  halfnq  9654  ltrnq  9657  archnq  9658  addclprlem2  9695  prlem934  9711  prlem936  9725  addcmpblnr  9746  mulcmpblnrlem  9747  ltsrpr  9754  m1p1sr  9769  m1m1sr  9770  0idsr  9774  1idsr  9775  00sr  9776  pn0sr  9778  recexsrlem  9780  mulgt0sr  9782  sqgt0sr  9783  mulresr  9816  axmulcom  9832  axmulass  9834  axdistr  9835  axi2m1  9836  ax1rid  9838  axcnre  9841  mul02lem1  10063  addid1  10067  negid  10179  negsub  10180  subneg  10181  negsubdii  10217  muleqadd  10520  crne0  10860  2p2e4  10991  3p2e5  11007  3p3e6  11008  4p2e6  11009  4p3e7  11010  4p4e8  11011  5p2e7  11012  5p3e8  11013  5p4e9  11014  5p5e10OLD  11015  6p2e8  11016  6p3e9  11017  6p4e10OLD  11018  7p2e9  11019  7p3e10OLD  11020  8p2e10OLD  11021  3t3e9  11027  8th4div3  11099  halfpm6th  11100  addltmul  11115  div4p1lem1div2  11134  nn0n0n1ge2  11205  nneo  11293  zeo  11295  numsuc  11343  numltc  11360  numsucc  11381  numma  11389  nummul1c  11394  decrmac  11409  decsubi  11415  decsubiOLD  11416  decmul1  11417  decmul10add  11425  decmul10addOLD  11426  6p5lem  11427  5p5e10  11428  6p4e10  11430  7p3e10  11435  8p2e10  11442  4t3lem  11463  9t11e99  11503  9t11e99OLD  11504  decbin2  11515  xmulmnf1  11935  fztp  12222  fzprval  12226  fztpval  12227  fzshftral  12252  fz0tp  12264  fz0to3un2pr  12265  fzo01  12372  fzo12sn  12373  fzo13pr  12374  fzo0to2pr  12375  fzo0to3tp  12376  fzo0to42pr  12377  fzo1to4tp  12378  quoremz  12471  quoremnn0ALT  12473  intfrac2  12474  intfracq  12475  sqval  12739  sqrecii  12763  sq4e2t8  12779  cu2  12780  i3  12783  i4  12784  binom2i  12791  binom3  12802  crreczi  12806  3dec  12867  sq10OLD  12868  3decOLD  12870  nn0opthlem1  12872  facp1  12882  faclbnd  12894  faclbnd2  12895  faclbnd4lem1  12897  faclbnd4lem4  12900  bcn1  12917  bcn2  12923  4bc3eq4  12932  4bc2eq6  12933  hashgadd  12979  hashxplem  13032  hashmap  13034  hashfun  13036  hashbclem  13045  fz1isolem  13054  ccatlid  13168  ccatrid  13169  ccats1val2  13202  ccat2s1p2  13204  wrdeqs1cat  13272  swrdccatin12lem3  13287  swrdccat3a  13291  cats1fvn  13400  cats1cat  13403  cats2cat  13404  s3fn  13452  swrds2  13479  reim0  13652  cji  13693  sqrtm1  13810  absi  13820  rddif  13874  iseraltlem2  14207  iseralt  14209  fsump1i  14288  fsummulc2  14304  incexclem  14353  incexc  14354  arisum2  14378  geoihalfsum  14399  mertenslem1  14401  mertens  14403  risefall0lem  14542  risefac1  14549  fallfac1  14550  fallfacfwd  14552  bpoly0  14566  bpoly1  14567  bpolydiflem  14570  bpoly2  14573  bpoly3  14574  bpoly4  14575  fsumcube  14576  ef0lem  14594  ege2le3  14605  eft0val  14627  ef4p  14628  efgt1p2  14629  efgt1p  14630  tanval2  14648  efival  14667  ef01bndlem  14699  sin01bnd  14700  cos01bnd  14701  cos1bnd  14702  cos2bnd  14703  rpnnen2lem11  14738  sqr2irrlem  14762  3dvdsdec  14838  3dvdsdecOLD  14839  3dvds2dec  14840  3dvds2decOLD  14841  odd2np1lem  14848  odd2np1  14849  oddp1even  14852  opoe  14871  divalglem5  14904  divalglem6  14905  bits0  14934  0bits  14945  gcdaddmlem  15029  6gcd4e2  15039  lcmneg  15100  3lcm2e6woprm  15112  6lcm4e12  15113  3prm  15190  3lcm2e6  15224  phiprm  15266  eulerthlem2  15271  prmdiv  15274  pythagtriplem12  15315  pythagtriplem14  15317  pcmpt  15380  pcfac  15387  prmpwdvds  15392  pockthi  15395  prmreclem2  15405  prmreclem6  15409  4sqlem5  15430  4sqlem13  15445  modxai  15556  mod2xnegi  15559  gcdi  15561  decexp2  15563  numexpp1  15566  numexp2x  15567  decsplit0b  15568  decsplit1  15570  decsplit  15571  decsplit0bOLD  15572  decsplit1OLD  15574  decsplitOLD  15575  2exp16  15581  prmlem0  15596  139prm  15615  163prm  15616  317prm  15617  631prm  15618  1259lem4  15625  1259lem5  15626  1259prm  15627  2503lem1  15628  2503lem2  15629  2503lem3  15630  2503prm  15631  4001lem1  15632  4001lem4  15635  ressinbas  15709  rcaninv  16223  rescfth  16366  xpccatid  16597  oduval  16899  oppgmnd  17553  psgnunilem2  17684  psgnunilem4  17686  psgnpmtr  17699  psgn0fv0  17700  psgnsn  17709  psgnprfval1  17711  lsmmod2  17858  efgi0  17902  efgi1  17903  efginvrel2  17909  efgsval2  17915  efgsp1  17919  efgredleme  17925  efgredlemc  17927  efgcpbllemb  17937  frgpnabllem1  18045  lt6abl  18065  gsumconstf  18104  gsum2dlem2  18139  pwsgsum  18147  fsfnn0gsumfsffz  18148  dprd0  18199  dprdf1  18201  dprd2da  18210  ablfac1lem  18236  pgpfac1lem3  18245  pgpfaclem1  18249  srgbinomlem4  18312  opprring  18400  mulgass3  18406  evlsval  19286  mpff  19300  ply1assa  19336  gsumply1subr  19371  ply1coe  19433  coe1fzgsumdlem  19438  coe1fzgsumd  19439  gsumply1eq  19442  evl1gsumdlem  19487  evl1gsumd  19488  xrsnsgrp  19547  znbas  19656  znzrh2  19658  dsmmval2  19841  frlmip  19878  matgsum  20004  madetsumid  20028  mdetrsca  20170  mdetrsca2  20171  mdettpos  20178  m2detleiblem2  20195  madugsum  20210  madurid  20211  cpmat  20275  pmatcollpwfi  20348  pmatcollpw3fi1lem1  20352  pm2mpval  20361  mp2pm2mplem5  20376  chpmat1dlem  20401  chpmat1d  20402  chpidmat  20413  cpmidpmat  20439  cpmadugsumfi  20443  chcoeffeqlem  20451  cayleyhamilton0  20455  cayleyhamiltonALT  20457  cayleyhamilton1  20458  restin  20722  imacmp  20952  concompcon  20987  uptx  21180  cnpflf2  21556  tmdgsum2  21652  tsmsres  21699  tsmsf1o  21700  tsmsmhm  21701  prdsxmet  21925  resspwsds  21928  prdsxmslem2  22085  metdcn2  22382  metdcn  22383  metdscn2  22399  iimulcn  22476  icchmeo  22479  xrhmeo  22484  cnrehmeo  22491  cnheiborlem  22492  evth  22497  evth2  22498  lebnumlem2  22500  reparphti  22536  pcoass  22563  pi1xfrcnv  22596  ipcau2  22762  minveclem4  22928  pjthlem1  22933  ovolunlem1a  22988  unmbl  23029  uniioombl  23080  iblitg  23258  dfitg  23259  itg0  23269  iblcnlem1  23277  itgcnlem  23279  itgabs  23324  limcdif  23363  limccnp  23378  limccnp2  23379  dvexp  23439  dvmptid  23443  dvmptc  23444  dvmptfsum  23459  dveflem  23463  dvsincos  23465  mvth  23476  dvlipcn  23478  dvivthlem1  23492  dvfsumle  23505  dvfsumlem2  23511  itgsubst  23533  tdeglem4  23541  tdeglem2  23542  plypf1  23689  plymullem1  23691  coesub  23734  dgrmulc  23748  fta1lem  23783  vieta1lem1  23786  vieta1lem2  23787  aalioulem4  23811  aaliou3lem3  23820  abelthlem2  23907  abelthlem8  23914  abelthlem9  23915  sinhalfpilem  23936  efhalfpi  23944  cospi  23945  efipi  23946  sin2pi  23948  cos2pi  23949  ef2pi  23950  sin2pim  23958  cos2pim  23959  sinmpi  23960  cosmpi  23961  sinppi  23962  cosppi  23963  sincosq4sgn  23974  tangtx  23978  sincos4thpi  23986  sincos6thpi  23988  sincos3rdpi  23989  pige3  23990  abssinper  23991  efif1olem4  24012  efifo  24014  eff1o  24016  circgrp  24019  circsubm  24020  logneg  24055  logimul  24081  logneg2  24082  dvrelog  24100  logcnlem4  24108  dvlog  24114  dvlog2  24116  logtayl  24123  1cxp  24135  ecxp  24136  cxpsqrt  24166  dvsqrt  24200  dvcnsqrt  24202  root1eq1  24213  cxpeq  24215  elogb  24225  ang180lem1  24256  ang180lem2  24257  heron  24282  1cubrlem  24285  1cubr  24286  dcubic2  24288  mcubic  24291  cubic2  24292  binom4  24294  dquartlem1  24295  dquartlem2  24296  dquart  24297  quart1lem  24299  quart1  24300  quartlem1  24301  asinsin  24336  asin1  24338  acos1  24339  atanlogsublem  24359  atanlogsub  24360  efiatan2  24361  2efiatan  24362  tanatan  24363  atanbnd  24370  atan1  24372  dvatan  24379  atantayl2  24382  leibpilem2  24385  leibpi  24386  log2cnv  24388  log2tlbnd  24389  log2ublem1  24390  log2ublem2  24391  log2ublem3  24392  log2ub  24393  birthday  24398  amgmlem  24433  emcllem5  24443  lgamgulmlem2  24473  lgamgulmlem5  24476  lgam1  24507  wilthlem2  24512  ftalem6  24521  basellem2  24525  basellem3  24526  basellem5  24528  basellem8  24531  cht1  24608  chp1  24610  1sgmprm  24641  ppiublem2  24645  ppiub  24646  chtublem  24653  chtub  24654  logfacbnd3  24665  bcp1ctr  24721  bclbnd  24722  bposlem1  24726  bposlem4  24729  bposlem6  24731  bposlem8  24733  bposlem9  24734  lgslem1  24739  lgsdir2lem1  24767  lgsdir2lem2  24768  lgsdir2lem3  24769  lgsdir2lem5  24771  lgs1  24783  gausslemma2dlem1a  24807  gausslemma2dlem3  24810  gausslemma2dlem4  24811  gausslemma2d  24816  lgseisenlem1  24817  lgseisenlem3  24819  lgsquadlem1  24822  lgsquadlem2  24823  lgsquad2lem2  24827  m1lgs  24830  2lgslem1a2  24832  2sqlem8  24868  2sqblem  24873  logdivsum  24939  mulog2sumlem2  24941  log2sumbnd  24950  selberglem1  24951  selberglem2  24952  pntrmax  24970  pntibndlem2  24997  pntibndlem3  24998  pntlemg  25004  pntlemr  25008  pntlemo  25013  ostth2lem3  25041  ostth2lem4  25042  istrkg3ld  25077  trgcgrg  25128  tgcgr4  25144  colperpexlem1  25340  ax5seglem7  25533  axlowdimlem4  25543  axlowdimlem16  25555  0wlk  25841  0trl  25842  wlkntrllem2  25856  wlkntrl  25858  constr1trl  25884  1pthonlem1  25885  constr2wlk  25894  constr2trl  25895  wlkdvspthlem  25903  constr3trllem3  25946  constr3trllem4  25947  constr3trllem5  25948  constr3pthlem1  25949  constr3pthlem3  25951  clwwlkn2  26069  clwlkisclwwlk2  26084  wwlkext2clwwlk  26097  vdgr1c  26198  nbhashuvtx1  26208  vdegp1ai  26277  vdegp1bi  26278  vdegp1ci  26279  extwwlkfablem2  26371  numclwwlkovf2ex  26379  numclwlk2lem2f  26396  frgraregord013  26411  ex-exp  26465  ex-bc  26467  ex-gcd  26472  ex-lcm  26473  ex-ind-dvds  26476  smcnlem  26737  ipidsq  26753  dipcj  26757  dip0r  26760  nmlnoubi  26841  nmblolbii  26844  blocnilem  26849  ip1ilem  26871  ip2i  26873  ipdirilem  26874  ipasslem10  26884  ipasslem11  26885  siilem1  26896  hvmul0  27071  hvsubsub4i  27106  hvnegdii  27109  hvsubeq0i  27110  hvsubcan2i  27111  hvsubaddi  27113  hvsub0  27123  hisubcomi  27151  normlem0  27156  normlem1  27157  normlem2  27158  normlem3  27159  normlem9  27165  norm-ii-i  27184  norm3difi  27194  normpari  27201  polid2i  27204  polidi  27205  bcsiALT  27226  pjhthlem1  27440  chdmm3i  27528  chdmm4i  27529  chjidm  27569  chj4i  27572  chjjdiri  27573  spanunsni  27628  pjoml4i  27636  cmcm2i  27642  qlax4i  27679  qlax5i  27680  pjadjii  27723  pjmulii  27726  pjsubii  27727  pjssmii  27730  pjcji  27733  pjneli  27772  hoadd32i  27827  ho0subi  27844  hosubid1  27847  hosd2i  27872  hopncani  27873  hosubeq0i  27875  lnopeq0lem1  28054  lnopunilem1  28059  lnophmlem2  28066  nmbdoplbi  28073  nmcopexi  28076  lnfnmuli  28093  nmcfnexi  28100  nmoptri2i  28148  nmopcoadji  28150  golem1  28320  mdsl1i  28370  cvmdi  28373  mdslmd3i  28381  csmdsymi  28383  xrge00  28823  archirngz  28880  archiabllem2c  28886  gsumle  28916  gsummpt2co  28917  gsumvsca1  28919  gsumvsca2  28920  xrge0slmod  28981  psgnfzto1st  28992  lmat22det  29022  madjusmdetlem4  29030  raddcn  29109  xrge0iifhom  29117  xrge0mulc1cn  29121  cbvesum  29237  gsumesum  29254  esumpfinvallem  29269  esumpfinvalf  29271  dya2icoseg  29472  sitg0  29541  eulerpartlemd  29561  eulerpartlemgvv  29571  eulerpartlemgh  29573  fib0  29594  fib1  29595  fibp1  29596  orrvcval4  29659  orrvcoel  29660  orrvccel  29661  coinflipprob  29674  coinflippvt  29679  ballotlem2  29683  ballotth  29732  signstf0  29777  signstfvn  29778  signsvtn0  29779  signstfvp  29780  signstfveq0  29786  signsvf0  29789  signsvf1  29790  signsvfn  29791  signshf  29797  subfacp1lem1  30221  subfacp1lem5  30226  subfacval2  30229  subfaclim  30230  subfacval3  30231  cvxpcon  30284  cvxscon  30285  mrsub0  30473  problem4  30622  quad3  30624  sinccvglem  30626  iexpire  30680  faclimlem1  30688  frrlem5  30834  fwddifnp1  31248  knoppcnlem10  31468  knoppndvlem7  31485  knoppndvlem21  31499  cnndvlem1  31504  finxpreclem4  32203  ptrest  32374  poimirlem27  32402  dvtan  32426  itgabsnc  32445  ftc1anclem8  32458  dvasin  32462  dvacos  32463  areacirclem1  32466  areacirclem4  32469  areacirc  32471  prdstotbnd  32559  prdsbnd2  32560  repwsmet  32599  rrnequiv  32600  reheibor  32604  dalem-cly  33771  pmodN  33950  cdleme0cp  34315  cdleme0cq  34316  cdleme1  34328  cdleme3d  34332  cdleme3h  34336  cdleme4  34339  cdleme5  34341  cdleme7a  34344  cdleme8  34351  cdleme9  34354  cdleme10  34355  cdleme11g  34366  cdleme15b  34376  cdleme21  34439  cdleme22e  34446  cdleme22eALTN  34447  cdleme23c  34453  cdleme25cv  34460  cdleme35b  34552  cdleme35c  34553  cdleme42a  34573  cdleme42d  34575  cdleme43aN  34591  cdlemeg46gfv  34632  cdlemk35  35014  dihjatcclem1  35521  lcdval2  35693  mapdpglem21  35795  mapfzcons  36093  mapfzcons1cl  36095  2rexfrabdioph  36174  3rexfrabdioph  36175  4rexfrabdioph  36176  6rexfrabdioph  36177  7rexfrabdioph  36178  rabdiophlem2  36180  diophren  36191  rabren3dioph  36193  pellexlem5  36211  pell1qr1  36249  rmspecfund  36288  jm2.17a  36341  jm2.17b  36342  jm2.27c  36388  jm2.27dlem5  36394  lmhmlnmsplit  36471  arearect  36616  areaquad  36617  relexp2  36784  trclfvdecomr  36835  k0004val0  37268  inductionexd  37269  unitadd  37316  amgm2d  37319  amgm3d  37320  lhe4.4ex1a  37346  expgrowthi  37350  expgrowth  37352  bccn1  37361  binomcxplemdvbinom  37370  binomcxplemdvsum  37372  binomcxplemnotnn0  37373  binomcxp  37374  refsumcn  38008  unirnmapsn  38197  oddfl  38226  infleinflem2  38325  sumnnodd  38494  cosnegpi  38547  dvcosre  38596  dvsinax  38598  ioodvbdlimc1lem2  38619  ioodvbdlimc2lem  38621  dvmptmulf  38624  dvxpaek  38627  dvmptfprod  38632  dvnprodlem2  38634  dvnprodlem3  38635  itgsin0pilem1  38638  itgsinexplem1  38642  itgsubsticclem  38664  stoweidlem13  38703  wallispilem4  38758  wallispi2lem1  38761  wallispi2lem2  38762  stirlinglem1  38764  dirkerper  38786  dirkertrigeqlem1  38788  dirkertrigeqlem3  38790  dirkertrigeq  38791  dirkeritg  38792  dirkercncflem1  38793  dirkercncflem2  38794  fourierdlem36  38833  fourierdlem41  38838  fourierdlem42  38839  fourierdlem48  38844  fourierdlem56  38852  fourierdlem57  38853  fourierdlem58  38854  fourierdlem60  38856  fourierdlem61  38857  fourierdlem62  38858  fourierdlem65  38861  fourierdlem73  38869  fourierdlem80  38876  fourierdlem87  38883  fourierdlem89  38885  fourierdlem90  38886  fourierdlem91  38887  fourierdlem100  38896  fourierdlem103  38899  fourierdlem107  38903  fourierdlem112  38908  fourierdlem113  38909  fourierdlem115  38911  fouriercnp  38916  sqwvfoura  38918  sqwvfourb  38919  fourierswlem  38920  fouriersw  38921  etransclem2  38926  etransclem37  38961  etransclem46  38970  hoidmvlelem3  39284  vonioolem2  39369  issmflem  39410  smfmullem2  39474  1t10e1p1e11  39735  1t10e1p1e11OLD  39736  fmtno0  39788  fmtno1  39789  fmtnorec2lem  39790  fmtnorec3  39796  fmtno2  39798  fmtno3  39799  fmtno4  39800  fmtno4sqrt  39819  fmtno4prmfac  39820  2exp5  39843  139prmALT  39847  31prm  39848  2exp7  39850  2exp11  39853  mod42tp1mod8  39855  lighneallem2  39859  5tcu2e40  39868  3exp4mod41  39869  41prothprmlem1  39870  41prothprmlem2  39871  41prothprm  39872  bits0ALTV  39926  nnsum3primes4  40002  nnsum3primesgbe  40006  nnsum4primesodd  40010  nnsum4primesoddALTV  40011  nnsum4primeseven  40014  nnsum4primesevenALTV  40015  bgoldbtbndlem1  40019  tgoldbachlt  40028  tgoldbachltOLD  40035  pfx1  40072  pfxccatpfx1  40088  pfxccatpfx2  40089  uhgrstrrepe  40299  vdegp1ci-av  40749  1wlkp1lem6  40882  1wlkp1lem8  40884  1wlkp1  40885  uhgr1wlkspthlem2  40955  pthdlem1  40967  pthdlem2  40969  pthd  40970  crctcsh1wlkn0lem4  41011  crctcsh1wlkn0lem5  41012  crctcsh1wlkn0lem6  41013  crctcshlem4  41018  crctcsh1wlkn0  41019  21wlkdlem2  41128  21wlkdlem4  41130  2pthdlem1  41132  clwlkclwwlk2  41207  wwlksext2clwwlk  41226  0ewlk  41277  1ewlk  41278  01wlk  41279  1pthdlem1  41297  1pthdlem2  41298  11wlkdlem1  41299  11wlkdlem4  41302  1wlk2v2e  41319  31wlkdlem2  41322  31wlkdlem4  41324  3pthdlem1  41326  eupth0  41377  eupthp1  41379  eucrctshift  41406  eucrct2eupth  41408  av-extwwlkfablem1  41503  av-extwwlkfablem2  41505  av-numclwwlkovf2ex  41512  av-numclwlk2lem2f  41528  av-frgraregord013  41544  2t6m3t4e0  41914  zlmodzxzequa  42074  zlmodzxznm  42075  zlmodzxzequap  42077  nn0sumshdiglemA  42206  nn0sumshdiglemB  42207  nn0sumshdiglem1  42208  sec0  42256  dfdp2OLD  42263  amgmw2d  42315
  Copyright terms: Public domain W3C validator