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

Theorem oveq2i 5789
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 5786 . 2  |-  ( A  =  B  ->  ( C F A )  =  ( C F B ) )
31, 2ax-mp 10 1  |-  ( C F A )  =  ( C F B )
Colors of variables: wff set class
Syntax hints:    = wceq 1619  (class class class)co 5778
This theorem is referenced by:  caov32  5967  caov4  5971  caov42  5973  seqomsuc  6423  oa1suc  6484  om1  6494  oe1  6496  oawordeulem  6506  oeoalem  6548  nnm1  6600  nnm2  6601  nneob  6604  omopthlem1  6607  mapsnconst  6767  mapsncnv  6768  map2xp  6985  cantnflt  7327  cnfcom2  7359  infxpenc  7599  infxpenc2  7603  ackbij1lem5  7804  alephom  8161  pwxpndom2  8241  adderpqlem  8532  addassnq  8536  mulcanenq  8538  distrnq  8539  ltanq  8549  ltexnq  8553  halfnq  8554  ltrnq  8557  archnq  8558  addclprlem2  8595  prlem934  8611  prlem936  8625  addcmpblnr  8648  mulcmpblnrlem  8649  ltsrpr  8653  m1p1sr  8668  m1m1sr  8669  0idsr  8673  1idsr  8674  00sr  8675  pn0sr  8677  recexsrlem  8679  mulgt0sr  8681  sqgt0sr  8682  mulresr  8715  axmulcom  8731  axmulass  8733  axdistr  8734  axi2m1  8735  ax1rid  8737  axcnre  8740  mul02lem1  8942  addid1  8946  add42i  8986  negid  9048  negsub  9049  subneg  9050  negsubdii  9085  muleqadd  9366  crne0  9693  2p2e4  9795  3p2e5  9808  3p3e6  9809  4p2e6  9810  4p3e7  9811  4p4e8  9812  5p2e7  9813  5p3e8  9814  5p4e9  9815  5p5e10  9816  6p2e8  9817  6p3e9  9818  6p4e10  9819  7p2e9  9820  7p3e10  9821  8p2e10  9822  3t3e9  9826  8th4div3  9888  halfpm6th  9889  addltmul  9900  nneo  10048  zeo  10050  numsuc  10089  numltc  10097  numsucc  10103  numma  10108  nummul1c  10113  6p5lem  10126  4t3lem  10148  decbin2  10181  xmulmnf1  10548  fztp  10793  fzprval  10796  fztpval  10797  fzshftral  10821  fzo01  10865  quoremz  10911  quoremnn0  10913  intfrac2  10914  intfracq  10915  sqval  11115  sqrecii  11138  cu2  11153  i3  11156  i4  11157  binom2i  11164  binom3  11174  crreczi  11178  nn0opthlem1  11235  facp1  11245  faclbnd  11255  faclbnd2  11256  faclbnd4lem1  11258  faclbnd4lem4  11261  bcn1  11277  bcn2  11283  hashgadd  11311  hashxplem  11336  hashmap  11338  hashfun  11340  hashbclem  11341  fz1isolem  11350  ccatlid  11385  ccatrid  11386  eqs1  11398  wrdeqs1cat  11426  cats1un  11427  cats1fvn  11459  cats1cat  11462  swrds2  11511  reim0  11554  cji  11595  sqrm1  11712  absi  11722  rddif  11775  iseraltlem2  12106  iseralt  12108  fsump1i  12183  fsummulc2  12197  arisum2  12267  geoihalfsum  12286  mertenslem1  12288  mertens  12290  ef0lem  12308  ege2le3  12319  eft0val  12340  ef4p  12341  efgt1p2  12342  efgt1p  12343  tanval2  12361  efival  12380  ef01bndlem  12412  sin01bnd  12413  cos01bnd  12414  cos1bnd  12415  cos2bnd  12416  rpnnen2lem11  12451  sqr2irrlem  12474  odd2np1lem  12534  odd2np1  12535  oddp1even  12537  divalglem5  12544  divalglem6  12545  bits0  12567  0bits  12578  bitsinv1lem  12580  gcdaddmlem  12655  3prm  12723  phiprm  12793  eulerthlem2  12798  prmdiv  12801  opoe  12812  pythagtriplem12  12827  pythagtriplem14  12829  pcmpt  12888  pcfac  12895  prmpwdvds  12899  pockthi  12902  prmreclem2  12912  prmreclem6  12916  4sqlem5  12937  4sqlem13  12952  modxai  13031  mod2xnegi  13034  gcdi  13036  decexp2  13038  numexpp1  13041  numexp2x  13042  decsplit0b  13043  decsplit1  13045  decsplit  13046  2exp6  13049  2exp16  13051  prmlem0  13055  139prm  13073  163prm  13074  317prm  13075  631prm  13076  1259lem1  13077  1259lem3  13079  1259lem4  13080  1259lem5  13081  1259prm  13082  2503lem1  13083  2503lem2  13084  2503lem3  13085  2503prm  13086  4001lem1  13087  4001lem2  13088  4001lem3  13089  4001lem4  13090  ressinbas  13152  rescfth  13759  xpccatid  13910  oduval  14182  oppgmnd  14775  lsmmod2  14933  efgi0  14977  efgi1  14978  efginvrel2  14984  efgsval2  14990  efgsp1  14994  efgredleme  15000  efgredlemc  15002  efgcpbllemb  15012  frgpnabllem1  15109  lt6abl  15129  gsumsn  15168  gsum2d  15171  pwsgsum  15178  dprd0  15214  dprdf1  15216  dprd2da  15225  ablfac1lem  15251  pgpfac1lem3  15260  pgpfaclem1  15264  opprrng  15361  mulgass3  15367  ply1assa  16226  ply1coe  16316  zlmval  16418  znbas  16445  znzrh2  16447  restin  16845  imacmp  17072  concompcon  17106  uptx  17267  cnpflf2  17643  tmdgsum2  17727  tsmsres  17774  tsmsf1o  17775  tsmsmhm  17776  prdsxmet  17881  resspwsds  17884  prdsxmslem2  18023  metdcn2  18292  metdcn  18293  metdscn2  18309  iimulcn  18384  icchmeo  18387  xrhmeo  18392  cnrehmeo  18399  cnheiborlem  18400  evth  18405  evth2  18406  lebnumlem2  18408  reparphti  18443  pcoass  18470  pi1xfrcnv  18503  ipcau2  18612  minveclem4  18744  pjthlem1  18749  ovolunlem1a  18803  unmbl  18843  uniioombl  18892  iblitg  19071  dfitg  19072  itg0  19082  iblcnlem1  19090  itgcnlem  19092  itgabs  19137  limcdif  19174  limccnp  19189  limccnp2  19190  dvexp  19250  dvmptid  19254  dvmptc  19255  dvmptfsum  19270  dveflem  19274  dvsincos  19276  mvth  19287  dvlipcn  19289  dvivthlem1  19303  dvfsumle  19316  dvfsumlem2  19322  itgsubst  19344  evlsval  19351  mpff  19373  tdeglem4  19394  tdeglem2  19395  plypf1  19542  plymullem1  19544  coesub  19586  dgrmulc  19600  fta1lem  19635  vieta1lem1  19638  vieta1lem2  19639  aalioulem4  19663  aaliou3lem3  19672  abelthlem2  19756  abelthlem8  19763  abelthlem9  19764  sinhalfpilem  19782  efhalfpi  19787  cospi  19788  efipi  19789  sin2pi  19791  cos2pi  19792  ef2pi  19793  sin2pim  19801  cos2pim  19802  sinmpi  19803  cosmpi  19804  sinppi  19805  cosppi  19806  sincosq4sgn  19817  tangtx  19821  sincos4thpi  19829  sincos6thpi  19831  sincos3rdpi  19832  pige3  19833  abssinper  19834  efif1olem4  19855  efifo  19857  eff1o  19859  logneg  19889  logimul  19916  logneg2  19917  dvrelog  19932  logcnlem4  19940  dvlog  19946  dvlog2  19948  logtayl  19955  1cxp  19967  ecxp  19968  cxpsqr  19998  dvsqr  20032  root1eq1  20043  cxpeq  20045  ang180lem1  20055  ang180lem2  20056  1cubrlem  20085  1cubr  20086  dcubic2  20088  mcubic  20091  cubic2  20092  binom4  20094  dquartlem1  20095  dquartlem2  20096  dquart  20097  quart1lem  20099  quart1  20100  quartlem1  20101  asinsin  20136  asin1  20138  acos1  20139  atanlogsublem  20159  atanlogsub  20160  efiatan2  20161  2efiatan  20162  tanatan  20163  atanbnd  20170  atan1  20172  dvatan  20179  atantayl2  20182  leibpilem2  20185  leibpi  20186  log2cnv  20188  log2tlbnd  20189  log2ublem1  20190  log2ublem2  20191  log2ublem3  20192  log2ub  20193  birthday  20197  amgmlem  20232  emcllem5  20241  wilthlem2  20255  ftalem6  20263  basellem2  20267  basellem3  20268  basellem5  20270  basellem8  20273  cht1  20351  chp1  20353  1sgmprm  20386  ppiublem2  20390  ppiub  20391  chtublem  20398  chtub  20399  logfacbnd3  20410  bcp1ctr  20466  bclbnd  20467  bposlem1  20471  bposlem4  20474  bposlem6  20476  bposlem8  20478  bposlem9  20479  lgslem1  20483  lgsdir2lem1  20510  lgsdir2lem2  20511  lgsdir2lem3  20512  lgsdir2lem5  20514  lgs1  20525  lgseisenlem1  20536  lgseisenlem3  20538  lgsquadlem1  20541  lgsquadlem2  20542  lgsquad2lem2  20546  m1lgs  20549  2sqlem8  20559  2sqblem  20564  logdivsum  20630  mulog2sumlem2  20632  log2sumbnd  20641  selberglem1  20642  selberglem2  20643  pntrmax  20661  pntibndlem2  20688  pntibndlem3  20689  pntlemg  20695  pntlemr  20699  pntlemo  20704  ostth2lem3  20732  ostth2lem4  20733  smcnlem  21216  ipidsq  21232  dipcj  21236  dip0r  21239  nmlnoubi  21320  nmblolbii  21323  blocnilem  21328  ip1ilem  21350  ip2i  21352  ipdirilem  21353  ipasslem10  21363  ipasslem11  21364  siilem1  21375  hvmul0  21549  hvsubsub4i  21584  hvnegdii  21587  hvsubeq0i  21588  hvsubcan2i  21589  hvsubaddi  21591  hvsub0  21601  hisubcomi  21629  normlem0  21634  normlem1  21635  normlem2  21636  normlem3  21637  normlem9  21643  norm-ii-i  21662  norm3difi  21672  normpari  21679  polid2i  21682  polidi  21683  bcsiALT  21704  pjhthlem1  21916  chdmm3i  22004  chdmm4i  22005  chjidm  22045  chj4i  22048  chjjdiri  22049  spanunsni  22104  pjoml4i  22130  cmcm2i  22136  qlax4i  22173  qlax5i  22174  pjadjii  22217  pjmulii  22220  pjsubii  22221  pjssmii  22224  pjcji  22227  pjneli  22266  hoadd32i  22304  ho0subi  22321  hosubid1  22324  hosd2i  22349  hopncani  22350  hosubeq0i  22352  lnopeq0lem1  22531  lnopunilem1  22536  lnophmlem2  22543  nmbdoplbi  22550  nmcopexi  22553  lnfnmuli  22570  nmcfnexi  22577  nmoptri2i  22625  nmopcoadji  22627  golem1  22797  mdsl1i  22847  cvmdi  22850  mdslmd3i  22858  csmdsymi  22860  ballotlem2  22994  ballotth  23043  subfacp1lem1  23068  subfacp1lem5  23073  subfacval2  23076  subfaclim  23077  subfacval3  23078  cvxpcon  23131  cvxscon  23132  vdgr1c  23254  vdegp1ai  23266  vdegp1bi  23267  vdegp1ci  23268  sinccvglem  23363  4bc3eq4  23455  4bc2eq6  23456  frrlem5  23640  ax5seglem7  23924  axlowdimlem4  23934  axlowdimlem16  23946  bpoly0  24146  bpoly1  24147  bpolydiflem  24150  bpoly2  24153  bpoly3  24154  bpoly4  24155  fsumcube  24156  geme2  24628  nfwpr4c  24638  tolat  24639  fprodp1fi  24681  limfilnei  24914  1cat  25112  dualcat2  25137  isntr  25226  intset  25397  fnckle  25398  prdstotbnd  25871  prdsbnd2  25872  repwsmet  25911  rrnequiv  25912  reheibor  25916  mapfzcons  26146  mapfzcons1cl  26148  2rexfrabdioph  26230  3rexfrabdioph  26231  4rexfrabdioph  26232  6rexfrabdioph  26233  7rexfrabdioph  26234  rabdiophlem2  26236  diophren  26249  rabren3dioph  26251  pellexlem5  26271  pell1qr1  26309  rmspecfund  26347  jm2.17a  26400  jm2.17b  26401  jm2.27c  26453  jm2.27dlem5  26459  lmhmlnmsplit  26538  dsmmval2  26555  psgnunilem2  26771  psgnunilem4  26773  psgnpmtr  26786  lhe4.4ex1a  26899  expgrowthi  26903  expgrowth  26905  refsumcn  27055  stoweidlem13  27083  sec0  27263  dalem-cly  29011  pmodN  29190  cdleme0cp  29554  cdleme0cq  29555  cdleme1  29567  cdleme3d  29571  cdleme3h  29575  cdleme4  29578  cdleme5  29580  cdleme7a  29583  cdleme8  29590  cdleme9  29593  cdleme10  29594  cdleme11g  29605  cdleme15b  29615  cdleme21  29677  cdleme22e  29684  cdleme22eALTN  29685  cdleme23c  29691  cdleme25cv  29698  cdleme35b  29790  cdleme35c  29791  cdleme42a  29811  cdleme42d  29813  cdleme43aN  29829  cdlemeg46gfv  29870  cdlemk35  30252  dihjatcclem1  30759  lcdval2  30931  mapdpglem21  31033
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1927  ax-ext 2237
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 941  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1884  df-clab 2243  df-cleq 2249  df-clel 2252  df-nfc 2381  df-rex 2522  df-rab 2525  df-v 2759  df-dif 3116  df-un 3118  df-in 3120  df-ss 3127  df-nul 3417  df-if 3526  df-sn 3606  df-pr 3607  df-op 3609  df-uni 3788  df-br 3984  df-opab 4038  df-xp 4661  df-cnv 4663  df-dm 4665  df-rn 4666  df-res 4667  df-ima 4668  df-fv 4675  df-ov 5781
  Copyright terms: Public domain W3C validator