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

Theorem oveq2i 6051
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 6048 . 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 1649  (class class class)co 6040
This theorem is referenced by:  caov32  6233  caov4  6237  caov42  6239  seqomsuc  6673  oa1suc  6734  om1  6744  oe1  6746  oawordeulem  6756  oeoalem  6798  nnm1  6850  nnm2  6851  nneob  6854  omopthlem1  6857  mapsnconst  7018  mapsncnv  7019  map2xp  7236  cantnflt  7583  cnfcom2  7615  infxpenc  7855  infxpenc2  7859  ackbij1lem5  8060  alephom  8416  pwxpndom2  8496  adderpqlem  8787  addassnq  8791  mulcanenq  8793  distrnq  8794  ltanq  8804  ltexnq  8808  halfnq  8809  ltrnq  8812  archnq  8813  addclprlem2  8850  prlem934  8866  prlem936  8880  addcmpblnr  8903  mulcmpblnrlem  8904  ltsrpr  8908  m1p1sr  8923  m1m1sr  8924  0idsr  8928  1idsr  8929  00sr  8930  pn0sr  8932  recexsrlem  8934  mulgt0sr  8936  sqgt0sr  8937  mulresr  8970  axmulcom  8986  axmulass  8988  axdistr  8989  axi2m1  8990  ax1rid  8992  axcnre  8995  mul02lem1  9198  addid1  9202  add42i  9242  negid  9304  negsub  9305  subneg  9306  negsubdii  9341  muleqadd  9622  crne0  9949  2p2e4  10054  3p2e5  10067  3p3e6  10068  4p2e6  10069  4p3e7  10070  4p4e8  10071  5p2e7  10072  5p3e8  10073  5p4e9  10074  5p5e10  10075  6p2e8  10076  6p3e9  10077  6p4e10  10078  7p2e9  10079  7p3e10  10080  8p2e10  10081  3t3e9  10085  8th4div3  10147  halfpm6th  10148  addltmul  10159  nn0n0n1ge2  10236  nneo  10309  zeo  10311  numsuc  10350  numltc  10358  numsucc  10364  numma  10369  nummul1c  10374  6p5lem  10387  4t3lem  10409  decbin2  10442  xmulmnf1  10811  fztp  11058  fz0tp  11059  fzprval  11062  fztpval  11063  fzshftral  11089  fzo01  11137  fzo12sn  11138  fzo0to2pr  11139  fzo0to3tp  11140  fzo0to42pr  11141  quoremz  11191  quoremnn0ALT  11193  intfrac2  11194  intfracq  11195  sqval  11396  sqrecii  11419  cu2  11434  i3  11437  i4  11438  binom2i  11445  binom3  11455  crreczi  11459  nn0opthlem1  11516  facp1  11526  faclbnd  11536  faclbnd2  11537  faclbnd4lem1  11539  faclbnd4lem4  11542  bcn1  11559  bcn2  11565  hashgadd  11606  hashxplem  11651  hashmap  11653  hashfun  11655  hashbclem  11656  fz1isolem  11665  ccatlid  11703  ccatrid  11704  eqs1  11716  wrdeqs1cat  11744  cats1un  11745  cats1fvn  11777  cats1cat  11780  swrds2  11835  reim0  11878  cji  11919  sqrm1  12036  absi  12046  rddif  12099  iseraltlem2  12431  iseralt  12433  fsump1i  12508  fsummulc2  12522  incexclem  12571  incexc  12572  arisum2  12595  geoihalfsum  12614  mertenslem1  12616  mertens  12618  ef0lem  12636  ege2le3  12647  eft0val  12668  ef4p  12669  efgt1p2  12670  efgt1p  12671  tanval2  12689  efival  12708  ef01bndlem  12740  sin01bnd  12741  cos01bnd  12742  cos1bnd  12743  cos2bnd  12744  rpnnen2lem11  12779  sqr2irrlem  12802  odd2np1lem  12862  odd2np1  12863  oddp1even  12865  divalglem5  12872  divalglem6  12873  bits0  12895  0bits  12906  gcdaddmlem  12983  3prm  13051  phiprm  13121  eulerthlem2  13126  prmdiv  13129  opoe  13140  pythagtriplem12  13155  pythagtriplem14  13157  pcmpt  13216  pcfac  13223  prmpwdvds  13227  pockthi  13230  prmreclem2  13240  prmreclem6  13244  4sqlem5  13265  4sqlem13  13280  modxai  13359  mod2xnegi  13362  gcdi  13364  decexp2  13366  numexpp1  13369  numexp2x  13370  decsplit0b  13371  decsplit1  13373  decsplit  13374  2exp6  13377  2exp16  13379  prmlem0  13383  139prm  13401  163prm  13402  317prm  13403  631prm  13404  1259lem1  13405  1259lem3  13407  1259lem4  13408  1259lem5  13409  1259prm  13410  2503lem1  13411  2503lem2  13412  2503lem3  13413  2503prm  13414  4001lem1  13415  4001lem2  13416  4001lem3  13417  4001lem4  13418  ressinbas  13480  rescfth  14089  xpccatid  14240  oduval  14512  oppgmnd  15105  lsmmod2  15263  efgi0  15307  efgi1  15308  efginvrel2  15314  efgsval2  15320  efgsp1  15324  efgredleme  15330  efgredlemc  15332  efgcpbllemb  15342  frgpnabllem1  15439  lt6abl  15459  gsumsn  15498  gsum2d  15501  pwsgsum  15508  dprd0  15544  dprdf1  15546  dprd2da  15555  ablfac1lem  15581  pgpfac1lem3  15590  pgpfaclem1  15594  opprrng  15691  mulgass3  15697  ply1assa  16552  ply1coe  16639  zlmval  16752  znbas  16779  znzrh2  16781  restin  17184  imacmp  17414  concompcon  17448  uptx  17610  cnpflf2  17985  tmdgsum2  18079  tsmsres  18126  tsmsf1o  18127  tsmsmhm  18128  prdsxmet  18352  resspwsds  18355  prdsxmslem2  18512  metdcn2  18823  metdcn  18824  metdscn2  18840  iimulcn  18916  icchmeo  18919  xrhmeo  18924  cnrehmeo  18931  cnheiborlem  18932  evth  18937  evth2  18938  lebnumlem2  18940  reparphti  18975  pcoass  19002  pi1xfrcnv  19035  ipcau2  19144  minveclem4  19286  pjthlem1  19291  ovolunlem1a  19345  unmbl  19385  uniioombl  19434  iblitg  19613  dfitg  19614  itg0  19624  iblcnlem1  19632  itgcnlem  19634  itgabs  19679  limcdif  19716  limccnp  19731  limccnp2  19732  dvexp  19792  dvmptid  19796  dvmptc  19797  dvmptfsum  19812  dveflem  19816  dvsincos  19818  mvth  19829  dvlipcn  19831  dvivthlem1  19845  dvfsumle  19858  dvfsumlem2  19864  itgsubst  19886  evlsval  19893  mpff  19915  tdeglem4  19936  tdeglem2  19937  plypf1  20084  plymullem1  20086  coesub  20128  dgrmulc  20142  fta1lem  20177  vieta1lem1  20180  vieta1lem2  20181  aalioulem4  20205  aaliou3lem3  20214  abelthlem2  20301  abelthlem8  20308  abelthlem9  20309  sinhalfpilem  20327  efhalfpi  20332  cospi  20333  efipi  20334  sin2pi  20336  cos2pi  20337  ef2pi  20338  sin2pim  20346  cos2pim  20347  sinmpi  20348  cosmpi  20349  sinppi  20350  cosppi  20351  sincosq4sgn  20362  tangtx  20366  sincos4thpi  20374  sincos6thpi  20376  sincos3rdpi  20377  pige3  20378  abssinper  20379  efif1olem4  20400  efifo  20402  eff1o  20404  logneg  20435  logimul  20462  logneg2  20463  dvrelog  20481  logcnlem4  20489  dvlog  20495  dvlog2  20497  logtayl  20504  1cxp  20516  ecxp  20517  cxpsqr  20547  dvsqr  20581  root1eq1  20592  cxpeq  20594  ang180lem1  20604  ang180lem2  20605  1cubrlem  20634  1cubr  20635  dcubic2  20637  mcubic  20640  cubic2  20641  binom4  20643  dquartlem1  20644  dquartlem2  20645  dquart  20646  quart1lem  20648  quart1  20649  quartlem1  20650  asinsin  20685  asin1  20687  acos1  20688  atanlogsublem  20708  atanlogsub  20709  efiatan2  20710  2efiatan  20711  tanatan  20712  atanbnd  20719  atan1  20721  dvatan  20728  atantayl2  20731  leibpilem2  20734  leibpi  20735  log2cnv  20737  log2tlbnd  20738  log2ublem1  20739  log2ublem2  20740  log2ublem3  20741  log2ub  20742  birthday  20746  amgmlem  20781  emcllem5  20791  wilthlem2  20805  ftalem6  20813  basellem2  20817  basellem3  20818  basellem5  20820  basellem8  20823  cht1  20901  chp1  20903  1sgmprm  20936  ppiublem2  20940  ppiub  20941  chtublem  20948  chtub  20949  logfacbnd3  20960  bcp1ctr  21016  bclbnd  21017  bposlem1  21021  bposlem4  21024  bposlem6  21026  bposlem8  21028  bposlem9  21029  lgslem1  21033  lgsdir2lem1  21060  lgsdir2lem2  21061  lgsdir2lem3  21062  lgsdir2lem5  21064  lgs1  21075  lgseisenlem1  21086  lgseisenlem3  21088  lgsquadlem1  21091  lgsquadlem2  21092  lgsquad2lem2  21096  m1lgs  21099  2sqlem8  21109  2sqblem  21114  logdivsum  21180  mulog2sumlem2  21182  log2sumbnd  21191  selberglem1  21192  selberglem2  21193  pntrmax  21211  pntibndlem2  21238  pntibndlem3  21239  pntlemg  21245  pntlemr  21249  pntlemo  21254  ostth2lem3  21282  ostth2lem4  21283  0wlk  21498  0trl  21499  wlkntrllem2  21513  wlkntrl  21515  constr1trl  21541  1pthonlem1  21542  constr2wlk  21551  constr2trl  21552  wlkdvspthlem  21560  constr3trllem3  21592  constr3trllem4  21593  constr3trllem5  21594  constr3pthlem1  21595  constr3pthlem3  21597  vdgr1c  21629  vdegp1ai  21659  vdegp1bi  21660  vdegp1ci  21661  smcnlem  22146  ipidsq  22162  dipcj  22166  dip0r  22169  nmlnoubi  22250  nmblolbii  22253  blocnilem  22258  ip1ilem  22280  ip2i  22282  ipdirilem  22283  ipasslem10  22293  ipasslem11  22294  siilem1  22305  hvmul0  22479  hvsubsub4i  22514  hvnegdii  22517  hvsubeq0i  22518  hvsubcan2i  22519  hvsubaddi  22521  hvsub0  22531  hisubcomi  22559  normlem0  22564  normlem1  22565  normlem2  22566  normlem3  22567  normlem9  22573  norm-ii-i  22592  norm3difi  22602  normpari  22609  polid2i  22612  polidi  22613  bcsiALT  22634  pjhthlem1  22846  chdmm3i  22934  chdmm4i  22935  chjidm  22975  chj4i  22978  chjjdiri  22979  spanunsni  23034  pjoml4i  23042  cmcm2i  23048  qlax4i  23085  qlax5i  23086  pjadjii  23129  pjmulii  23132  pjsubii  23133  pjssmii  23136  pjcji  23139  pjneli  23178  hoadd32i  23234  ho0subi  23251  hosubid1  23254  hosd2i  23279  hopncani  23280  hosubeq0i  23282  lnopeq0lem1  23461  lnopunilem1  23466  lnophmlem2  23473  nmbdoplbi  23480  nmcopexi  23483  lnfnmuli  23500  nmcfnexi  23507  nmoptri2i  23555  nmopcoadji  23557  golem1  23727  mdsl1i  23777  cvmdi  23780  mdslmd3i  23788  csmdsymi  23790  xrge00  24161  gsumconstf  24175  raddcn  24268  xrge0iifhom  24276  xrge0mulc1cn  24280  cbvesum  24391  gsumesum  24404  esumpfinvallem  24417  esumpfinvalf  24419  dya2icoseg  24580  orrvcval4  24675  orrvcoel  24676  orrvccel  24677  coinflipprob  24690  coinflippvt  24695  ballotlem2  24699  ballotth  24748  lgamgulmlem2  24767  lgamgulmlem5  24770  lgam1  24801  subfacp1lem1  24818  subfacp1lem5  24823  subfacval2  24826  subfaclim  24827  subfacval3  24828  cvxpcon  24882  cvxscon  24883  sinccvglem  25062  4bc3eq4  25156  4bc2eq6  25157  risefall0lem  25294  risefac1  25299  fallfac1  25300  fallfacfwd  25303  faclimlem1  25310  frrlem5  25499  ax5seglem7  25778  axlowdimlem4  25788  axlowdimlem16  25800  bpoly0  26000  bpoly1  26001  bpolydiflem  26004  bpoly2  26007  bpoly3  26008  bpoly4  26009  fsumcube  26010  itgabsnc  26173  dvreasin  26179  areacirclem2  26181  areacirclem5  26185  areacirc  26187  prdstotbnd  26393  prdsbnd2  26394  repwsmet  26433  rrnequiv  26434  reheibor  26438  mapfzcons  26662  mapfzcons1cl  26664  2rexfrabdioph  26746  3rexfrabdioph  26747  4rexfrabdioph  26748  6rexfrabdioph  26749  7rexfrabdioph  26750  rabdiophlem2  26752  diophren  26764  rabren3dioph  26766  pellexlem5  26786  pell1qr1  26824  rmspecfund  26862  jm2.17a  26915  jm2.17b  26916  jm2.27c  26968  jm2.27dlem5  26974  lmhmlnmsplit  27053  dsmmval2  27070  psgnunilem2  27286  psgnunilem4  27288  psgnpmtr  27301  lhe4.4ex1a  27414  expgrowthi  27418  expgrowth  27420  refsumcn  27568  m1expeven  27592  dvcosre  27608  itgsin0pilem1  27611  itgsinexplem1  27615  stoweidlem13  27629  wallispilem4  27684  wallispi2lem1  27687  wallispi2lem2  27688  stirlinglem1  27690  f13idfv  27963  swrdccatin12lem4  28025  swrdccat3a  28030  sec0  28217  elogb  28246  dalem-cly  30153  pmodN  30332  cdleme0cp  30696  cdleme0cq  30697  cdleme1  30709  cdleme3d  30713  cdleme3h  30717  cdleme4  30720  cdleme5  30722  cdleme7a  30725  cdleme8  30732  cdleme9  30735  cdleme10  30736  cdleme11g  30747  cdleme15b  30757  cdleme21  30819  cdleme22e  30826  cdleme22eALTN  30827  cdleme23c  30833  cdleme25cv  30840  cdleme35b  30932  cdleme35c  30933  cdleme42a  30953  cdleme42d  30955  cdleme43aN  30971  cdlemeg46gfv  31012  cdlemk35  31394  dihjatcclem1  31901  lcdval2  32073  mapdpglem21  32175
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-rex 2672  df-rab 2675  df-v 2918  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-nul 3589  df-if 3700  df-sn 3780  df-pr 3781  df-op 3783  df-uni 3976  df-br 4173  df-iota 5377  df-fv 5421  df-ov 6043
  Copyright terms: Public domain W3C validator