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

Theorem oveq2i 6078
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 6075 . 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 1652  (class class class)co 6067
This theorem is referenced by:  caov32  6260  caov4  6264  caov42  6266  seqomsuc  6700  oa1suc  6761  om1  6771  oe1  6773  oawordeulem  6783  oeoalem  6825  nnm1  6877  nnm2  6878  nneob  6881  omopthlem1  6884  mapsnconst  7045  mapsncnv  7046  map2xp  7263  cantnflt  7611  cnfcom2  7643  infxpenc  7883  infxpenc2  7887  ackbij1lem5  8088  alephom  8444  pwxpndom2  8524  adderpqlem  8815  addassnq  8819  mulcanenq  8821  distrnq  8822  ltanq  8832  ltexnq  8836  halfnq  8837  ltrnq  8840  archnq  8841  addclprlem2  8878  prlem934  8894  prlem936  8908  addcmpblnr  8931  mulcmpblnrlem  8932  ltsrpr  8936  m1p1sr  8951  m1m1sr  8952  0idsr  8956  1idsr  8957  00sr  8958  pn0sr  8960  recexsrlem  8962  mulgt0sr  8964  sqgt0sr  8965  mulresr  8998  axmulcom  9014  axmulass  9016  axdistr  9017  axi2m1  9018  ax1rid  9020  axcnre  9023  mul02lem1  9226  addid1  9230  add42i  9270  negid  9332  negsub  9333  subneg  9334  negsubdii  9369  muleqadd  9650  crne0  9977  2p2e4  10082  3p2e5  10095  3p3e6  10096  4p2e6  10097  4p3e7  10098  4p4e8  10099  5p2e7  10100  5p3e8  10101  5p4e9  10102  5p5e10  10103  6p2e8  10104  6p3e9  10105  6p4e10  10106  7p2e9  10107  7p3e10  10108  8p2e10  10109  3t3e9  10113  8th4div3  10175  halfpm6th  10176  addltmul  10187  nn0n0n1ge2  10264  nneo  10337  zeo  10339  numsuc  10378  numltc  10386  numsucc  10392  numma  10397  nummul1c  10402  6p5lem  10415  4t3lem  10437  decbin2  10470  xmulmnf1  10839  fztp  11086  fz0tp  11087  fzprval  11090  fztpval  11091  fzshftral  11117  fzo01  11165  fzo12sn  11166  fzo0to2pr  11167  fzo0to3tp  11168  fzo0to42pr  11169  quoremz  11219  quoremnn0ALT  11221  intfrac2  11222  intfracq  11223  sqval  11424  sqrecii  11447  cu2  11462  i3  11465  i4  11466  binom2i  11473  binom3  11483  crreczi  11487  nn0opthlem1  11544  facp1  11554  faclbnd  11564  faclbnd2  11565  faclbnd4lem1  11567  faclbnd4lem4  11570  bcn1  11587  bcn2  11593  hashgadd  11634  hashxplem  11679  hashmap  11681  hashfun  11683  hashbclem  11684  fz1isolem  11693  ccatlid  11731  ccatrid  11732  eqs1  11744  wrdeqs1cat  11772  cats1un  11773  cats1fvn  11805  cats1cat  11808  swrds2  11863  reim0  11906  cji  11947  sqrm1  12064  absi  12074  rddif  12127  iseraltlem2  12459  iseralt  12461  fsump1i  12536  fsummulc2  12550  incexclem  12599  incexc  12600  arisum2  12623  geoihalfsum  12642  mertenslem1  12644  mertens  12646  ef0lem  12664  ege2le3  12675  eft0val  12696  ef4p  12697  efgt1p2  12698  efgt1p  12699  tanval2  12717  efival  12736  ef01bndlem  12768  sin01bnd  12769  cos01bnd  12770  cos1bnd  12771  cos2bnd  12772  rpnnen2lem11  12807  sqr2irrlem  12830  odd2np1lem  12890  odd2np1  12891  oddp1even  12893  divalglem5  12900  divalglem6  12901  bits0  12923  0bits  12934  gcdaddmlem  13011  3prm  13079  phiprm  13149  eulerthlem2  13154  prmdiv  13157  opoe  13168  pythagtriplem12  13183  pythagtriplem14  13185  pcmpt  13244  pcfac  13251  prmpwdvds  13255  pockthi  13258  prmreclem2  13268  prmreclem6  13272  4sqlem5  13293  4sqlem13  13308  modxai  13387  mod2xnegi  13390  gcdi  13392  decexp2  13394  numexpp1  13397  numexp2x  13398  decsplit0b  13399  decsplit1  13401  decsplit  13402  2exp6  13405  2exp16  13407  prmlem0  13411  139prm  13429  163prm  13430  317prm  13431  631prm  13432  1259lem1  13433  1259lem3  13435  1259lem4  13436  1259lem5  13437  1259prm  13438  2503lem1  13439  2503lem2  13440  2503lem3  13441  2503prm  13442  4001lem1  13443  4001lem2  13444  4001lem3  13445  4001lem4  13446  ressinbas  13508  rescfth  14117  xpccatid  14268  oduval  14540  oppgmnd  15133  lsmmod2  15291  efgi0  15335  efgi1  15336  efginvrel2  15342  efgsval2  15348  efgsp1  15352  efgredleme  15358  efgredlemc  15360  efgcpbllemb  15370  frgpnabllem1  15467  lt6abl  15487  gsumsn  15526  gsum2d  15529  pwsgsum  15536  dprd0  15572  dprdf1  15574  dprd2da  15583  ablfac1lem  15609  pgpfac1lem3  15618  pgpfaclem1  15622  opprrng  15719  mulgass3  15725  ply1assa  16580  ply1coe  16667  zlmval  16780  znbas  16807  znzrh2  16809  restin  17213  imacmp  17443  concompcon  17478  uptx  17640  cnpflf2  18015  tmdgsum2  18109  tsmsres  18156  tsmsf1o  18157  tsmsmhm  18158  prdsxmet  18382  resspwsds  18385  prdsxmslem2  18542  metdcn2  18853  metdcn  18854  metdscn2  18870  iimulcn  18946  icchmeo  18949  xrhmeo  18954  cnrehmeo  18961  cnheiborlem  18962  evth  18967  evth2  18968  lebnumlem2  18970  reparphti  19005  pcoass  19032  pi1xfrcnv  19065  ipcau2  19174  minveclem4  19316  pjthlem1  19321  ovolunlem1a  19375  unmbl  19415  uniioombl  19464  iblitg  19643  dfitg  19644  itg0  19654  iblcnlem1  19662  itgcnlem  19664  itgabs  19709  limcdif  19746  limccnp  19761  limccnp2  19762  dvexp  19822  dvmptid  19826  dvmptc  19827  dvmptfsum  19842  dveflem  19846  dvsincos  19848  mvth  19859  dvlipcn  19861  dvivthlem1  19875  dvfsumle  19888  dvfsumlem2  19894  itgsubst  19916  evlsval  19923  mpff  19945  tdeglem4  19966  tdeglem2  19967  plypf1  20114  plymullem1  20116  coesub  20158  dgrmulc  20172  fta1lem  20207  vieta1lem1  20210  vieta1lem2  20211  aalioulem4  20235  aaliou3lem3  20244  abelthlem2  20331  abelthlem8  20338  abelthlem9  20339  sinhalfpilem  20357  efhalfpi  20362  cospi  20363  efipi  20364  sin2pi  20366  cos2pi  20367  ef2pi  20368  sin2pim  20376  cos2pim  20377  sinmpi  20378  cosmpi  20379  sinppi  20380  cosppi  20381  sincosq4sgn  20392  tangtx  20396  sincos4thpi  20404  sincos6thpi  20406  sincos3rdpi  20407  pige3  20408  abssinper  20409  efif1olem4  20430  efifo  20432  eff1o  20434  logneg  20465  logimul  20492  logneg2  20493  dvrelog  20511  logcnlem4  20519  dvlog  20525  dvlog2  20527  logtayl  20534  1cxp  20546  ecxp  20547  cxpsqr  20577  dvsqr  20611  root1eq1  20622  cxpeq  20624  ang180lem1  20634  ang180lem2  20635  1cubrlem  20664  1cubr  20665  dcubic2  20667  mcubic  20670  cubic2  20671  binom4  20673  dquartlem1  20674  dquartlem2  20675  dquart  20676  quart1lem  20678  quart1  20679  quartlem1  20680  asinsin  20715  asin1  20717  acos1  20718  atanlogsublem  20738  atanlogsub  20739  efiatan2  20740  2efiatan  20741  tanatan  20742  atanbnd  20749  atan1  20751  dvatan  20758  atantayl2  20761  leibpilem2  20764  leibpi  20765  log2cnv  20767  log2tlbnd  20768  log2ublem1  20769  log2ublem2  20770  log2ublem3  20771  log2ub  20772  birthday  20776  amgmlem  20811  emcllem5  20821  wilthlem2  20835  ftalem6  20843  basellem2  20847  basellem3  20848  basellem5  20850  basellem8  20853  cht1  20931  chp1  20933  1sgmprm  20966  ppiublem2  20970  ppiub  20971  chtublem  20978  chtub  20979  logfacbnd3  20990  bcp1ctr  21046  bclbnd  21047  bposlem1  21051  bposlem4  21054  bposlem6  21056  bposlem8  21058  bposlem9  21059  lgslem1  21063  lgsdir2lem1  21090  lgsdir2lem2  21091  lgsdir2lem3  21092  lgsdir2lem5  21094  lgs1  21105  lgseisenlem1  21116  lgseisenlem3  21118  lgsquadlem1  21121  lgsquadlem2  21122  lgsquad2lem2  21126  m1lgs  21129  2sqlem8  21139  2sqblem  21144  logdivsum  21210  mulog2sumlem2  21212  log2sumbnd  21221  selberglem1  21222  selberglem2  21223  pntrmax  21241  pntibndlem2  21268  pntibndlem3  21269  pntlemg  21275  pntlemr  21279  pntlemo  21284  ostth2lem3  21312  ostth2lem4  21313  0wlk  21528  0trl  21529  wlkntrllem2  21543  wlkntrl  21545  constr1trl  21571  1pthonlem1  21572  constr2wlk  21581  constr2trl  21582  wlkdvspthlem  21590  constr3trllem3  21622  constr3trllem4  21623  constr3trllem5  21624  constr3pthlem1  21625  constr3pthlem3  21627  vdgr1c  21659  vdegp1ai  21689  vdegp1bi  21690  vdegp1ci  21691  smcnlem  22176  ipidsq  22192  dipcj  22196  dip0r  22199  nmlnoubi  22280  nmblolbii  22283  blocnilem  22288  ip1ilem  22310  ip2i  22312  ipdirilem  22313  ipasslem10  22323  ipasslem11  22324  siilem1  22335  hvmul0  22509  hvsubsub4i  22544  hvnegdii  22547  hvsubeq0i  22548  hvsubcan2i  22549  hvsubaddi  22551  hvsub0  22561  hisubcomi  22589  normlem0  22594  normlem1  22595  normlem2  22596  normlem3  22597  normlem9  22603  norm-ii-i  22622  norm3difi  22632  normpari  22639  polid2i  22642  polidi  22643  bcsiALT  22664  pjhthlem1  22876  chdmm3i  22964  chdmm4i  22965  chjidm  23005  chj4i  23008  chjjdiri  23009  spanunsni  23064  pjoml4i  23072  cmcm2i  23078  qlax4i  23115  qlax5i  23116  pjadjii  23159  pjmulii  23162  pjsubii  23163  pjssmii  23166  pjcji  23169  pjneli  23208  hoadd32i  23264  ho0subi  23281  hosubid1  23284  hosd2i  23309  hopncani  23310  hosubeq0i  23312  lnopeq0lem1  23491  lnopunilem1  23496  lnophmlem2  23503  nmbdoplbi  23510  nmcopexi  23513  lnfnmuli  23530  nmcfnexi  23537  nmoptri2i  23585  nmopcoadji  23587  golem1  23757  mdsl1i  23807  cvmdi  23810  mdslmd3i  23818  csmdsymi  23820  xrge00  24191  gsumconstf  24205  raddcn  24298  xrge0iifhom  24306  xrge0mulc1cn  24310  cbvesum  24421  gsumesum  24434  esumpfinvallem  24447  esumpfinvalf  24449  dya2icoseg  24610  orrvcval4  24705  orrvcoel  24706  orrvccel  24707  coinflipprob  24720  coinflippvt  24725  ballotlem2  24729  ballotth  24778  lgamgulmlem2  24797  lgamgulmlem5  24800  lgam1  24831  subfacp1lem1  24848  subfacp1lem5  24853  subfacval2  24856  subfaclim  24857  subfacval3  24858  cvxpcon  24912  cvxscon  24913  sinccvglem  25092  4bc3eq4  25186  4bc2eq6  25187  risefall0lem  25326  risefac1  25333  fallfac1  25334  fallfacfwd  25336  faclimlem1  25346  frrlem5  25535  ax5seglem7  25817  axlowdimlem4  25827  axlowdimlem16  25839  bpoly0  26039  bpoly1  26040  bpolydiflem  26043  bpoly2  26046  bpoly3  26047  bpoly4  26048  fsumcube  26049  itgabsnc  26215  dvreasin  26221  areacirclem2  26223  areacirclem5  26227  areacirc  26229  prdstotbnd  26435  prdsbnd2  26436  repwsmet  26475  rrnequiv  26476  reheibor  26480  mapfzcons  26704  mapfzcons1cl  26706  2rexfrabdioph  26788  3rexfrabdioph  26789  4rexfrabdioph  26790  6rexfrabdioph  26791  7rexfrabdioph  26792  rabdiophlem2  26794  diophren  26806  rabren3dioph  26808  pellexlem5  26828  pell1qr1  26866  rmspecfund  26904  jm2.17a  26957  jm2.17b  26958  jm2.27c  27010  jm2.27dlem5  27016  lmhmlnmsplit  27095  dsmmval2  27112  psgnunilem2  27328  psgnunilem4  27330  psgnpmtr  27343  lhe4.4ex1a  27456  expgrowthi  27460  expgrowth  27462  refsumcn  27610  m1expeven  27634  dvcosre  27650  itgsin0pilem1  27653  itgsinexplem1  27657  stoweidlem13  27671  wallispilem4  27726  wallispi2lem1  27729  wallispi2lem2  27730  stirlinglem1  27732  f13idfv  28005  swrdccatin12lem4  28067  swrdccat3a  28072  sec0  28259  elogb  28288  dalem-cly  30199  pmodN  30378  cdleme0cp  30742  cdleme0cq  30743  cdleme1  30755  cdleme3d  30759  cdleme3h  30763  cdleme4  30766  cdleme5  30768  cdleme7a  30771  cdleme8  30778  cdleme9  30781  cdleme10  30782  cdleme11g  30793  cdleme15b  30803  cdleme21  30865  cdleme22e  30872  cdleme22eALTN  30873  cdleme23c  30879  cdleme25cv  30886  cdleme35b  30978  cdleme35c  30979  cdleme42a  30999  cdleme42d  31001  cdleme43aN  31017  cdlemeg46gfv  31058  cdlemk35  31440  dihjatcclem1  31947  lcdval2  32119  mapdpglem21  32221
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2411
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2417  df-cleq 2423  df-clel 2426  df-nfc 2555  df-rex 2698  df-rab 2701  df-v 2945  df-dif 3310  df-un 3312  df-in 3314  df-ss 3321  df-nul 3616  df-if 3727  df-sn 3807  df-pr 3808  df-op 3810  df-uni 4003  df-br 4200  df-iota 5404  df-fv 5448  df-ov 6070
  Copyright terms: Public domain W3C validator