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

Theorem oveq2i 5768
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 5765 . 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 5757
This theorem is referenced by:  caov32  5946  caov4  5950  caov42  5952  seqomsuc  6402  oa1suc  6463  om1  6473  oe1  6475  oawordeulem  6485  oeoalem  6527  nnm1  6579  nnm2  6580  nneob  6583  omopthlem1  6586  mapsnconst  6746  mapsncnv  6747  map2xp  6964  cantnflt  7306  cnfcom2  7338  infxpenc  7578  infxpenc2  7582  ackbij1lem5  7783  alephom  8140  pwxpndom2  8220  adderpqlem  8511  addassnq  8515  mulcanenq  8517  distrnq  8518  ltanq  8528  ltexnq  8532  halfnq  8533  ltrnq  8536  archnq  8537  addclprlem2  8574  prlem934  8590  prlem936  8604  addcmpblnr  8627  mulcmpblnrlem  8628  ltsrpr  8632  m1p1sr  8647  m1m1sr  8648  0idsr  8652  1idsr  8653  00sr  8654  pn0sr  8656  recexsrlem  8658  mulgt0sr  8660  sqgt0sr  8661  mulresr  8694  axmulcom  8710  axmulass  8712  axdistr  8713  axi2m1  8714  ax1rid  8716  axcnre  8719  mul02lem1  8921  addid1  8925  add42i  8965  negid  9027  negsub  9028  subneg  9029  negsubdii  9064  muleqadd  9345  crne0  9672  2p2e4  9774  3p2e5  9787  3p3e6  9788  4p2e6  9789  4p3e7  9790  4p4e8  9791  5p2e7  9792  5p3e8  9793  5p4e9  9794  5p5e10  9795  6p2e8  9796  6p3e9  9797  6p4e10  9798  7p2e9  9799  7p3e10  9800  8p2e10  9801  3t3e9  9805  8th4div3  9867  halfpm6th  9868  addltmul  9879  nneo  10027  zeo  10029  numsuc  10068  numltc  10076  numsucc  10082  numma  10087  nummul1c  10092  6p5lem  10105  4t3lem  10127  decbin2  10160  xmulmnf1  10527  fztp  10772  fzprval  10775  fztpval  10776  fzshftral  10800  fzo01  10844  quoremz  10890  quoremnn0  10892  intfrac2  10893  intfracq  10894  sqval  11094  sqrecii  11117  cu2  11132  i3  11135  i4  11136  binom2i  11143  binom3  11153  crreczi  11157  nn0opthlem1  11214  facp1  11224  faclbnd  11234  faclbnd2  11235  faclbnd4lem1  11237  faclbnd4lem4  11240  bcn1  11256  bcn2  11262  hashgadd  11290  hashxplem  11315  hashmap  11317  hashfun  11319  hashbclem  11320  fz1isolem  11329  ccatlid  11364  ccatrid  11365  eqs1  11377  wrdeqs1cat  11405  cats1un  11406  cats1fvn  11438  cats1cat  11441  swrds2  11490  reim0  11533  cji  11574  sqrm1  11691  absi  11701  rddif  11754  iseraltlem2  12085  iseralt  12087  fsump1i  12162  fsummulc2  12176  arisum2  12246  geoihalfsum  12265  mertenslem1  12267  mertens  12269  ef0lem  12287  ege2le3  12298  eft0val  12319  ef4p  12320  efgt1p2  12321  efgt1p  12322  tanval2  12340  efival  12359  ef01bndlem  12391  sin01bnd  12392  cos01bnd  12393  cos1bnd  12394  cos2bnd  12395  rpnnen2lem11  12430  sqr2irrlem  12453  odd2np1lem  12513  odd2np1  12514  oddp1even  12516  divalglem5  12523  divalglem6  12524  bits0  12546  0bits  12557  bitsinv1lem  12559  gcdaddmlem  12634  3prm  12702  phiprm  12772  eulerthlem2  12777  prmdiv  12780  opoe  12791  pythagtriplem12  12806  pythagtriplem14  12808  pcmpt  12867  pcfac  12874  prmpwdvds  12878  pockthi  12881  prmreclem2  12891  prmreclem6  12895  4sqlem5  12916  4sqlem13  12931  modxai  13010  mod2xnegi  13013  gcdi  13015  decexp2  13017  numexpp1  13020  numexp2x  13021  decsplit0b  13022  decsplit1  13024  decsplit  13025  2exp6  13028  2exp16  13030  prmlem0  13034  139prm  13052  163prm  13053  317prm  13054  631prm  13055  1259lem1  13056  1259lem3  13058  1259lem4  13059  1259lem5  13060  1259prm  13061  2503lem1  13062  2503lem2  13063  2503lem3  13064  2503prm  13065  4001lem1  13066  4001lem2  13067  4001lem3  13068  4001lem4  13069  ressinbas  13131  rescfth  13738  xpccatid  13889  oduval  14161  oppgmnd  14754  lsmmod2  14912  efgi0  14956  efgi1  14957  efginvrel2  14963  efgsval2  14969  efgsp1  14973  efgredleme  14979  efgredlemc  14981  efgcpbllemb  14991  frgpnabllem1  15088  lt6abl  15108  gsumsn  15147  gsum2d  15150  pwsgsum  15157  dprd0  15193  dprdf1  15195  dprd2da  15204  ablfac1lem  15230  pgpfac1lem3  15239  pgpfaclem1  15243  opprrng  15340  mulgass3  15346  ply1assa  16205  ply1coe  16295  zlmval  16397  znbas  16424  znzrh2  16426  restin  16824  imacmp  17051  concompcon  17085  uptx  17246  cnpflf2  17622  tmdgsum2  17706  tsmsres  17753  tsmsf1o  17754  tsmsmhm  17755  prdsxmet  17860  resspwsds  17863  prdsxmslem2  18002  metdcn2  18271  metdcn  18272  metdscn2  18288  iimulcn  18363  icchmeo  18366  xrhmeo  18371  cnrehmeo  18378  cnheiborlem  18379  evth  18384  evth2  18385  lebnumlem2  18387  reparphti  18422  pcoass  18449  pi1xfrcnv  18482  ipcau2  18591  minveclem4  18723  pjthlem1  18728  ovolunlem1a  18782  unmbl  18822  uniioombl  18871  iblitg  19050  dfitg  19051  itg0  19061  iblcnlem1  19069  itgcnlem  19071  itgabs  19116  limcdif  19153  limccnp  19168  limccnp2  19169  dvexp  19229  dvmptid  19233  dvmptc  19234  dvmptfsum  19249  dveflem  19253  dvsincos  19255  mvth  19266  dvlipcn  19268  dvivthlem1  19282  dvfsumle  19295  dvfsumlem2  19301  itgsubst  19323  evlsval  19330  mpff  19352  tdeglem4  19373  tdeglem2  19374  plypf1  19521  plymullem1  19523  coesub  19565  dgrmulc  19579  fta1lem  19614  vieta1lem1  19617  vieta1lem2  19618  aalioulem4  19642  aaliou3lem3  19651  abelthlem2  19735  abelthlem8  19742  abelthlem9  19743  sinhalfpilem  19761  efhalfpi  19766  cospi  19767  efipi  19768  sin2pi  19770  cos2pi  19771  ef2pi  19772  sin2pim  19780  cos2pim  19781  sinmpi  19782  cosmpi  19783  sinppi  19784  cosppi  19785  sincosq4sgn  19796  tangtx  19800  sincos4thpi  19808  sincos6thpi  19810  sincos3rdpi  19811  pige3  19812  abssinper  19813  efif1olem4  19834  efifo  19836  eff1o  19838  logneg  19868  logimul  19895  logneg2  19896  dvrelog  19911  logcnlem4  19919  dvlog  19925  dvlog2  19927  logtayl  19934  1cxp  19946  ecxp  19947  cxpsqr  19977  dvsqr  20011  root1eq1  20022  cxpeq  20024  ang180lem1  20034  ang180lem2  20035  1cubrlem  20064  1cubr  20065  dcubic2  20067  mcubic  20070  cubic2  20071  binom4  20073  dquartlem1  20074  dquartlem2  20075  dquart  20076  quart1lem  20078  quart1  20079  quartlem1  20080  asinsin  20115  asin1  20117  acos1  20118  atanlogsublem  20138  atanlogsub  20139  efiatan2  20140  2efiatan  20141  tanatan  20142  atanbnd  20149  atan1  20151  dvatan  20158  atantayl2  20161  leibpilem2  20164  leibpi  20165  log2cnv  20167  log2tlbnd  20168  log2ublem1  20169  log2ublem2  20170  log2ublem3  20171  log2ub  20172  birthday  20176  amgmlem  20211  emcllem5  20220  wilthlem2  20234  ftalem6  20242  basellem2  20246  basellem3  20247  basellem5  20249  basellem8  20252  cht1  20330  chp1  20332  1sgmprm  20365  ppiublem2  20369  ppiub  20370  chtublem  20377  chtub  20378  logfacbnd3  20389  bcp1ctr  20445  bclbnd  20446  bposlem1  20450  bposlem4  20453  bposlem6  20455  bposlem8  20457  bposlem9  20458  lgslem1  20462  lgsdir2lem1  20489  lgsdir2lem2  20490  lgsdir2lem3  20491  lgsdir2lem5  20493  lgs1  20504  lgseisenlem1  20515  lgseisenlem3  20517  lgsquadlem1  20520  lgsquadlem2  20521  lgsquad2lem2  20525  m1lgs  20528  2sqlem8  20538  2sqblem  20543  logdivsum  20609  mulog2sumlem2  20611  log2sumbnd  20620  selberglem1  20621  selberglem2  20622  pntrmax  20640  pntibndlem2  20667  pntibndlem3  20668  pntlemg  20674  pntlemr  20678  pntlemo  20683  ostth2lem3  20711  ostth2lem4  20712  smcnlem  21195  ipidsq  21211  dipcj  21215  dip0r  21218  nmlnoubi  21299  nmblolbii  21302  blocnilem  21307  ip1ilem  21329  ip2i  21331  ipdirilem  21332  ipasslem10  21342  ipasslem11  21343  siilem1  21354  hvmul0  21528  hvsubsub4i  21563  hvnegdii  21566  hvsubeq0i  21567  hvsubcan2i  21568  hvsubaddi  21570  hvsub0  21580  hisubcomi  21608  normlem0  21613  normlem1  21614  normlem2  21615  normlem3  21616  normlem9  21622  norm-ii-i  21641  norm3difi  21651  normpari  21658  polid2i  21661  polidi  21662  bcsiALT  21683  pjhthlem1  21895  chdmm3i  21983  chdmm4i  21984  chjidm  22024  chj4i  22027  chjjdiri  22028  spanunsni  22083  pjoml4i  22109  cmcm2i  22115  qlax4i  22152  qlax5i  22153  pjadjii  22196  pjmulii  22199  pjsubii  22200  pjssmii  22203  pjcji  22206  pjneli  22245  hoadd32i  22283  ho0subi  22300  hosubid1  22303  hosd2i  22328  hopncani  22329  hosubeq0i  22331  lnopeq0lem1  22510  lnopunilem1  22515  lnophmlem2  22522  nmbdoplbi  22529  nmcopexi  22532  lnfnmuli  22549  nmcfnexi  22556  nmoptri2i  22604  nmopcoadji  22606  golem1  22776  mdsl1i  22826  cvmdi  22829  mdslmd3i  22837  csmdsymi  22839  ballotlem2  22973  ballotth  23022  subfacp1lem1  23047  subfacp1lem5  23052  subfacval2  23055  subfaclim  23056  subfacval3  23057  cvxpcon  23110  cvxscon  23111  vdgr1c  23233  vdegp1ai  23245  vdegp1bi  23246  vdegp1ci  23247  sinccvglem  23342  4bc3eq4  23434  4bc2eq6  23435  frrlem5  23619  ax5seglem7  23903  axlowdimlem4  23913  axlowdimlem16  23925  bpoly0  24125  bpoly1  24126  bpolydiflem  24129  bpoly2  24132  bpoly3  24133  bpoly4  24134  fsumcube  24135  geme2  24607  nfwpr4c  24617  tolat  24618  fprodp1fi  24660  limfilnei  24893  1cat  25091  dualcat2  25116  isntr  25205  intset  25376  fnckle  25377  prdstotbnd  25850  prdsbnd2  25851  repwsmet  25890  rrnequiv  25891  reheibor  25895  mapfzcons  26125  mapfzcons1cl  26127  2rexfrabdioph  26209  3rexfrabdioph  26210  4rexfrabdioph  26211  6rexfrabdioph  26212  7rexfrabdioph  26213  rabdiophlem2  26215  diophren  26228  rabren3dioph  26230  pellexlem5  26250  pell1qr1  26288  rmspecfund  26326  jm2.17a  26379  jm2.17b  26380  jm2.27c  26432  jm2.27dlem5  26438  lmhmlnmsplit  26517  dsmmval2  26534  psgnunilem2  26750  psgnunilem4  26752  psgnpmtr  26765  lhe4.4ex1a  26878  expgrowthi  26882  expgrowth  26884  refsumcn  27034  stoweidlem13  27062  sec0  27242  dalem-cly  28990  pmodN  29169  cdleme0cp  29533  cdleme0cq  29534  cdleme1  29546  cdleme3d  29550  cdleme3h  29554  cdleme4  29557  cdleme5  29559  cdleme7a  29562  cdleme8  29569  cdleme9  29572  cdleme10  29573  cdleme11g  29584  cdleme15b  29594  cdleme21  29656  cdleme22e  29663  cdleme22eALTN  29664  cdleme23c  29670  cdleme25cv  29677  cdleme35b  29769  cdleme35c  29770  cdleme42a  29790  cdleme42d  29792  cdleme43aN  29808  cdlemeg46gfv  29849  cdlemk35  30231  dihjatcclem1  30738  lcdval2  30910  mapdpglem21  31012
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 2521  df-rab 2523  df-v 2742  df-dif 3097  df-un 3099  df-in 3101  df-ss 3108  df-nul 3398  df-if 3507  df-sn 3587  df-pr 3588  df-op 3590  df-uni 3769  df-br 3964  df-opab 4018  df-xp 4640  df-cnv 4642  df-dm 4644  df-rn 4645  df-res 4646  df-ima 4647  df-fv 4654  df-ov 5760
  Copyright terms: Public domain W3C validator