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

Theorem oveq2i 5831
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 5828 . 2  |-  ( A  =  B  ->  ( C F A )  =  ( C F B ) )
31, 2ax-mp 8 1  |-  ( C F A )  =  ( C F B )
Colors of variables: wff set class
Syntax hints:    = wceq 1623  (class class class)co 5820
This theorem is referenced by:  caov32  6009  caov4  6013  caov42  6015  seqomsuc  6465  oa1suc  6526  om1  6536  oe1  6538  oawordeulem  6548  oeoalem  6590  nnm1  6642  nnm2  6643  nneob  6646  omopthlem1  6649  mapsnconst  6809  mapsncnv  6810  map2xp  7027  cantnflt  7369  cnfcom2  7401  infxpenc  7641  infxpenc2  7645  ackbij1lem5  7846  alephom  8203  pwxpndom2  8283  adderpqlem  8574  addassnq  8578  mulcanenq  8580  distrnq  8581  ltanq  8591  ltexnq  8595  halfnq  8596  ltrnq  8599  archnq  8600  addclprlem2  8637  prlem934  8653  prlem936  8667  addcmpblnr  8690  mulcmpblnrlem  8691  ltsrpr  8695  m1p1sr  8710  m1m1sr  8711  0idsr  8715  1idsr  8716  00sr  8717  pn0sr  8719  recexsrlem  8721  mulgt0sr  8723  sqgt0sr  8724  mulresr  8757  axmulcom  8773  axmulass  8775  axdistr  8776  axi2m1  8777  ax1rid  8779  axcnre  8782  mul02lem1  8984  addid1  8988  add42i  9028  negid  9090  negsub  9091  subneg  9092  negsubdii  9127  muleqadd  9408  crne0  9735  2p2e4  9838  3p2e5  9851  3p3e6  9852  4p2e6  9853  4p3e7  9854  4p4e8  9855  5p2e7  9856  5p3e8  9857  5p4e9  9858  5p5e10  9859  6p2e8  9860  6p3e9  9861  6p4e10  9862  7p2e9  9863  7p3e10  9864  8p2e10  9865  3t3e9  9869  8th4div3  9931  halfpm6th  9932  addltmul  9943  nneo  10091  zeo  10093  numsuc  10132  numltc  10140  numsucc  10146  numma  10151  nummul1c  10156  6p5lem  10169  4t3lem  10191  decbin2  10224  xmulmnf1  10592  fztp  10837  fzprval  10840  fztpval  10841  fzshftral  10865  fzo01  10909  quoremz  10955  quoremnn0  10957  intfrac2  10958  intfracq  10959  sqval  11159  sqrecii  11182  cu2  11197  i3  11200  i4  11201  binom2i  11208  binom3  11218  crreczi  11222  nn0opthlem1  11279  facp1  11289  faclbnd  11299  faclbnd2  11300  faclbnd4lem1  11302  faclbnd4lem4  11305  bcn1  11321  bcn2  11327  hashgadd  11355  hashxplem  11381  hashmap  11383  hashfun  11385  hashbclem  11386  fz1isolem  11395  ccatlid  11430  ccatrid  11431  eqs1  11443  wrdeqs1cat  11471  cats1un  11472  cats1fvn  11504  cats1cat  11507  swrds2  11556  reim0  11599  cji  11640  sqrm1  11757  absi  11767  rddif  11820  iseraltlem2  12151  iseralt  12153  fsump1i  12228  fsummulc2  12242  incexclem  12291  incexc  12292  arisum2  12315  geoihalfsum  12334  mertenslem1  12336  mertens  12338  ef0lem  12356  ege2le3  12367  eft0val  12388  ef4p  12389  efgt1p2  12390  efgt1p  12391  tanval2  12409  efival  12428  ef01bndlem  12460  sin01bnd  12461  cos01bnd  12462  cos1bnd  12463  cos2bnd  12464  rpnnen2lem11  12499  sqr2irrlem  12522  odd2np1lem  12582  odd2np1  12583  oddp1even  12585  divalglem5  12592  divalglem6  12593  bits0  12615  0bits  12626  bitsinv1lem  12628  gcdaddmlem  12703  3prm  12771  phiprm  12841  eulerthlem2  12846  prmdiv  12849  opoe  12860  pythagtriplem12  12875  pythagtriplem14  12877  pcmpt  12936  pcfac  12943  prmpwdvds  12947  pockthi  12950  prmreclem2  12960  prmreclem6  12964  4sqlem5  12985  4sqlem13  13000  modxai  13079  mod2xnegi  13082  gcdi  13084  decexp2  13086  numexpp1  13089  numexp2x  13090  decsplit0b  13091  decsplit1  13093  decsplit  13094  2exp6  13097  2exp16  13099  prmlem0  13103  139prm  13121  163prm  13122  317prm  13123  631prm  13124  1259lem1  13125  1259lem3  13127  1259lem4  13128  1259lem5  13129  1259prm  13130  2503lem1  13131  2503lem2  13132  2503lem3  13133  2503prm  13134  4001lem1  13135  4001lem2  13136  4001lem3  13137  4001lem4  13138  ressinbas  13200  rescfth  13807  xpccatid  13958  oduval  14230  oppgmnd  14823  lsmmod2  14981  efgi0  15025  efgi1  15026  efginvrel2  15032  efgsval2  15038  efgsp1  15042  efgredleme  15048  efgredlemc  15050  efgcpbllemb  15060  frgpnabllem1  15157  lt6abl  15177  gsumsn  15216  gsum2d  15219  pwsgsum  15226  dprd0  15262  dprdf1  15264  dprd2da  15273  ablfac1lem  15299  pgpfac1lem3  15308  pgpfaclem1  15312  opprrng  15409  mulgass3  15415  ply1assa  16274  ply1coe  16364  zlmval  16466  znbas  16493  znzrh2  16495  restin  16893  imacmp  17120  concompcon  17154  uptx  17315  cnpflf2  17691  tmdgsum2  17775  tsmsres  17822  tsmsf1o  17823  tsmsmhm  17824  prdsxmet  17929  resspwsds  17932  prdsxmslem2  18071  metdcn2  18340  metdcn  18341  metdscn2  18357  iimulcn  18432  icchmeo  18435  xrhmeo  18440  cnrehmeo  18447  cnheiborlem  18448  evth  18453  evth2  18454  lebnumlem2  18456  reparphti  18491  pcoass  18518  pi1xfrcnv  18551  ipcau2  18660  minveclem4  18792  pjthlem1  18797  ovolunlem1a  18851  unmbl  18891  uniioombl  18940  iblitg  19119  dfitg  19120  itg0  19130  iblcnlem1  19138  itgcnlem  19140  itgabs  19185  limcdif  19222  limccnp  19237  limccnp2  19238  dvexp  19298  dvmptid  19302  dvmptc  19303  dvmptfsum  19318  dveflem  19322  dvsincos  19324  mvth  19335  dvlipcn  19337  dvivthlem1  19351  dvfsumle  19364  dvfsumlem2  19370  itgsubst  19392  evlsval  19399  mpff  19421  tdeglem4  19442  tdeglem2  19443  plypf1  19590  plymullem1  19592  coesub  19634  dgrmulc  19648  fta1lem  19683  vieta1lem1  19686  vieta1lem2  19687  aalioulem4  19711  aaliou3lem3  19720  abelthlem2  19804  abelthlem8  19811  abelthlem9  19812  sinhalfpilem  19830  efhalfpi  19835  cospi  19836  efipi  19837  sin2pi  19839  cos2pi  19840  ef2pi  19841  sin2pim  19849  cos2pim  19850  sinmpi  19851  cosmpi  19852  sinppi  19853  cosppi  19854  sincosq4sgn  19865  tangtx  19869  sincos4thpi  19877  sincos6thpi  19879  sincos3rdpi  19880  pige3  19881  abssinper  19882  efif1olem4  19903  efifo  19905  eff1o  19907  logneg  19937  logimul  19964  logneg2  19965  dvrelog  19980  logcnlem4  19988  dvlog  19994  dvlog2  19996  logtayl  20003  1cxp  20015  ecxp  20016  cxpsqr  20046  dvsqr  20080  root1eq1  20091  cxpeq  20093  ang180lem1  20103  ang180lem2  20104  1cubrlem  20133  1cubr  20134  dcubic2  20136  mcubic  20139  cubic2  20140  binom4  20142  dquartlem1  20143  dquartlem2  20144  dquart  20145  quart1lem  20147  quart1  20148  quartlem1  20149  asinsin  20184  asin1  20186  acos1  20187  atanlogsublem  20207  atanlogsub  20208  efiatan2  20209  2efiatan  20210  tanatan  20211  atanbnd  20218  atan1  20220  dvatan  20227  atantayl2  20230  leibpilem2  20233  leibpi  20234  log2cnv  20236  log2tlbnd  20237  log2ublem1  20238  log2ublem2  20239  log2ublem3  20240  log2ub  20241  birthday  20245  amgmlem  20280  emcllem5  20289  wilthlem2  20303  ftalem6  20311  basellem2  20315  basellem3  20316  basellem5  20318  basellem8  20321  cht1  20399  chp1  20401  1sgmprm  20434  ppiublem2  20438  ppiub  20439  chtublem  20446  chtub  20447  logfacbnd3  20458  bcp1ctr  20514  bclbnd  20515  bposlem1  20519  bposlem4  20522  bposlem6  20524  bposlem8  20526  bposlem9  20527  lgslem1  20531  lgsdir2lem1  20558  lgsdir2lem2  20559  lgsdir2lem3  20560  lgsdir2lem5  20562  lgs1  20573  lgseisenlem1  20584  lgseisenlem3  20586  lgsquadlem1  20589  lgsquadlem2  20590  lgsquad2lem2  20594  m1lgs  20597  2sqlem8  20607  2sqblem  20612  logdivsum  20678  mulog2sumlem2  20680  log2sumbnd  20689  selberglem1  20690  selberglem2  20691  pntrmax  20709  pntibndlem2  20736  pntibndlem3  20737  pntlemg  20743  pntlemr  20747  pntlemo  20752  ostth2lem3  20780  ostth2lem4  20781  smcnlem  21264  ipidsq  21280  dipcj  21284  dip0r  21287  nmlnoubi  21368  nmblolbii  21371  blocnilem  21376  ip1ilem  21398  ip2i  21400  ipdirilem  21401  ipasslem10  21411  ipasslem11  21412  siilem1  21423  hvmul0  21599  hvsubsub4i  21634  hvnegdii  21637  hvsubeq0i  21638  hvsubcan2i  21639  hvsubaddi  21641  hvsub0  21651  hisubcomi  21679  normlem0  21684  normlem1  21685  normlem2  21686  normlem3  21687  normlem9  21693  norm-ii-i  21712  norm3difi  21722  normpari  21729  polid2i  21732  polidi  21733  bcsiALT  21754  pjhthlem1  21966  chdmm3i  22054  chdmm4i  22055  chjidm  22095  chj4i  22098  chjjdiri  22099  spanunsni  22154  pjoml4i  22162  cmcm2i  22168  qlax4i  22205  qlax5i  22206  pjadjii  22249  pjmulii  22252  pjsubii  22253  pjssmii  22256  pjcji  22259  pjneli  22298  hoadd32i  22354  ho0subi  22371  hosubid1  22374  hosd2i  22399  hopncani  22400  hosubeq0i  22402  lnopeq0lem1  22581  lnopunilem1  22586  lnophmlem2  22593  nmbdoplbi  22600  nmcopexi  22603  lnfnmuli  22620  nmcfnexi  22627  nmoptri2i  22675  nmopcoadji  22677  golem1  22847  mdsl1i  22897  cvmdi  22900  mdslmd3i  22908  csmdsymi  22910  ballotlem2  23043  ballotth  23092  subfacp1lem1  23117  subfacp1lem5  23122  subfacval2  23125  subfaclim  23126  subfacval3  23127  cvxpcon  23180  cvxscon  23181  vdgr1c  23303  vdegp1ai  23315  vdegp1bi  23316  vdegp1ci  23317  sinccvglem  23412  4bc3eq4  23504  4bc2eq6  23505  frrlem5  23689  ax5seglem7  23973  axlowdimlem4  23983  axlowdimlem16  23995  bpoly0  24195  bpoly1  24196  bpolydiflem  24199  bpoly2  24202  bpoly3  24203  bpoly4  24204  fsumcube  24205  dvreasin  24333  areacirclem2  24335  areacirclem5  24339  areacirc  24341  geme2  24686  nfwpr4c  24696  tolat  24697  fprodp1fi  24739  limfilnei  24972  1cat  25170  dualcat2  25195  isntr  25284  intset  25455  fnckle  25456  prdstotbnd  25929  prdsbnd2  25930  repwsmet  25969  rrnequiv  25970  reheibor  25974  mapfzcons  26204  mapfzcons1cl  26206  2rexfrabdioph  26288  3rexfrabdioph  26289  4rexfrabdioph  26290  6rexfrabdioph  26291  7rexfrabdioph  26292  rabdiophlem2  26294  diophren  26307  rabren3dioph  26309  pellexlem5  26329  pell1qr1  26367  rmspecfund  26405  jm2.17a  26458  jm2.17b  26459  jm2.27c  26511  jm2.27dlem5  26517  lmhmlnmsplit  26596  dsmmval2  26613  psgnunilem2  26829  psgnunilem4  26831  psgnpmtr  26844  lhe4.4ex1a  26957  expgrowthi  26961  expgrowth  26963  refsumcn  27112  m1expeven  27136  dvcosre  27152  itgsin0pilem1  27155  itgsinexplem1  27159  stoweidlem13  27173  wallispilem4  27228  wallispi2lem1  27231  wallispi2lem2  27232  stirlinglem1  27234  sec0  27502  dalem-cly  29139  pmodN  29318  cdleme0cp  29682  cdleme0cq  29683  cdleme1  29695  cdleme3d  29699  cdleme3h  29703  cdleme4  29706  cdleme5  29708  cdleme7a  29711  cdleme8  29718  cdleme9  29721  cdleme10  29722  cdleme11g  29733  cdleme15b  29743  cdleme21  29805  cdleme22e  29812  cdleme22eALTN  29813  cdleme23c  29819  cdleme25cv  29826  cdleme35b  29918  cdleme35c  29919  cdleme42a  29939  cdleme42d  29941  cdleme43aN  29957  cdlemeg46gfv  29998  cdlemk35  30380  dihjatcclem1  30887  lcdval2  31059  mapdpglem21  31161
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1636  ax-8 1644  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1868  ax-ext 2265
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1631  df-clab 2271  df-cleq 2277  df-clel 2280  df-nfc 2409  df-rex 2550  df-rab 2553  df-v 2791  df-dif 3156  df-un 3158  df-in 3160  df-ss 3167  df-nul 3457  df-if 3567  df-sn 3647  df-pr 3648  df-op 3650  df-uni 3829  df-br 4025  df-opab 4079  df-xp 4694  df-cnv 4696  df-dm 4698  df-rn 4699  df-res 4700  df-ima 4701  df-fv 5229  df-ov 5823
  Copyright terms: Public domain W3C validator