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

Theorem oveq2i 5721
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 5718 . 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 5710
This theorem is referenced by:  caov32  5899  caov4  5903  caov42  5905  seqomsuc  6355  oa1suc  6416  om1  6426  oe1  6428  oawordeulem  6438  oeoalem  6480  nnm1  6532  nnm2  6533  nneob  6536  omopthlem1  6539  mapsnconst  6699  mapsncnv  6700  map2xp  6916  cantnflt  7257  cnfcom2  7289  infxpenc  7529  infxpenc2  7533  ackbij1lem5  7734  alephom  8087  pwxpndom2  8167  adderpqlem  8458  addassnq  8462  mulcanenq  8464  distrnq  8465  ltanq  8475  ltexnq  8479  halfnq  8480  ltrnq  8483  archnq  8484  addclprlem2  8521  prlem934  8537  prlem936  8551  addcmpblnr  8574  mulcmpblnrlem  8575  ltsrpr  8579  m1p1sr  8594  m1m1sr  8595  0idsr  8599  1idsr  8600  00sr  8601  pn0sr  8603  recexsrlem  8605  mulgt0sr  8607  sqgt0sr  8608  mulresr  8641  axmulcom  8657  axmulass  8659  axdistr  8660  axi2m1  8661  ax1rid  8663  axcnre  8666  mul02lem1  8868  addid1  8872  add42i  8912  negid  8974  negsub  8975  subneg  8976  negsubdii  9011  muleqadd  9292  crne0  9619  2p2e4  9721  3p2e5  9734  3p3e6  9735  4p2e6  9736  4p3e7  9737  4p4e8  9738  5p2e7  9739  5p3e8  9740  5p4e9  9741  5p5e10  9742  6p2e8  9743  6p3e9  9744  6p4e10  9745  7p2e9  9746  7p3e10  9747  8p2e10  9748  3t3e9  9752  8th4div3  9814  halfpm6th  9815  addltmul  9826  nneo  9974  zeo  9976  numsuc  10015  numltc  10023  numsucc  10029  numma  10034  nummul1c  10039  6p5lem  10052  4t3lem  10074  decbin2  10107  xmulmnf1  10474  fztp  10719  fzprval  10722  fztpval  10723  fzshftral  10747  fzo01  10791  quoremz  10837  quoremnn0  10839  intfrac2  10840  intfracq  10841  sqval  11041  sqrecii  11064  cu2  11079  i3  11082  i4  11083  binom2i  11090  binom3  11100  crreczi  11104  nn0opthlem1  11161  facp1  11171  faclbnd  11181  faclbnd2  11182  faclbnd4lem1  11184  faclbnd4lem4  11187  bcn1  11203  bcn2  11209  hashgadd  11237  hashxplem  11262  hashmap  11264  hashfun  11266  hashbclem  11267  fz1isolem  11276  ccatlid  11311  ccatrid  11312  eqs1  11324  wrdeqs1cat  11352  cats1un  11353  cats1fvn  11385  cats1cat  11388  swrds2  11437  reim0  11480  cji  11521  sqrm1  11638  absi  11648  rddif  11701  iseraltlem2  12032  iseralt  12034  fsump1i  12109  fsummulc2  12123  arisum2  12193  geoihalfsum  12212  mertenslem1  12214  mertens  12216  ef0lem  12234  ege2le3  12245  eft0val  12266  ef4p  12267  efgt1p2  12268  efgt1p  12269  tanval2  12287  efival  12306  ef01bndlem  12338  sin01bnd  12339  cos01bnd  12340  cos1bnd  12341  cos2bnd  12342  rpnnen2lem11  12377  sqr2irrlem  12400  odd2np1lem  12460  odd2np1  12461  oddp1even  12463  divalglem5  12470  divalglem6  12471  bits0  12493  0bits  12504  bitsinv1lem  12506  gcdaddmlem  12581  3prm  12649  phiprm  12719  eulerthlem2  12724  prmdiv  12727  opoe  12738  pythagtriplem12  12753  pythagtriplem14  12755  pcmpt  12814  pcfac  12821  prmpwdvds  12825  pockthi  12828  prmreclem2  12838  prmreclem6  12842  4sqlem5  12863  4sqlem13  12878  modxai  12957  mod2xnegi  12960  gcdi  12962  decexp2  12964  numexpp1  12967  numexp2x  12968  decsplit0b  12969  decsplit1  12971  decsplit  12972  2exp6  12975  2exp16  12977  prmlem0  12981  139prm  12999  163prm  13000  317prm  13001  631prm  13002  1259lem1  13003  1259lem3  13005  1259lem4  13006  1259lem5  13007  1259prm  13008  2503lem1  13009  2503lem2  13010  2503lem3  13011  2503prm  13012  4001lem1  13013  4001lem2  13014  4001lem3  13015  4001lem4  13016  ressinbas  13078  rescfth  13655  xpccatid  13806  oduval  14078  oppgmnd  14662  lsmmod2  14820  efgi0  14864  efgi1  14865  efginvrel2  14871  efgsval2  14877  efgsp1  14881  efgredleme  14887  efgredlemc  14889  efgcpbllemb  14899  frgpnabllem1  14996  lt6abl  15016  gsumsn  15055  gsum2d  15058  pwsgsum  15065  dprd0  15101  dprdf1  15103  dprd2da  15112  ablfac1lem  15138  pgpfac1lem3  15147  pgpfaclem1  15151  opprrng  15248  mulgass3  15254  ply1assa  16110  ply1coe  16200  zlmval  16302  znbas  16329  znzrh2  16331  restin  16729  imacmp  16956  concompcon  16990  uptx  17151  cnpflf2  17527  tmdgsum2  17611  tsmsres  17658  tsmsf1o  17659  tsmsmhm  17660  prdsxmet  17765  resspwsds  17768  prdsxmslem2  17907  metdcn2  18176  metdcn  18177  metdscn2  18193  iimulcn  18268  icchmeo  18271  xrhmeo  18276  cnrehmeo  18283  cnheiborlem  18284  evth  18289  evth2  18290  lebnumlem2  18292  reparphti  18327  pcoass  18354  pi1xfrcnv  18387  ipcau2  18496  minveclem4  18628  pjthlem1  18633  ovolunlem1a  18687  unmbl  18727  uniioombl  18776  iblitg  18955  dfitg  18956  itg0  18966  iblcnlem1  18974  itgcnlem  18976  itgabs  19021  limcdif  19058  limccnp  19073  limccnp2  19074  dvexp  19134  dvmptid  19138  dvmptc  19139  dvmptfsum  19154  dveflem  19158  dvsincos  19160  mvth  19171  dvlipcn  19173  dvivthlem1  19187  dvfsumle  19200  dvfsumlem2  19206  itgsubst  19228  evlsval  19235  mpff  19257  tdeglem4  19278  tdeglem2  19279  plypf1  19426  plymullem1  19428  coesub  19470  dgrmulc  19484  fta1lem  19519  vieta1lem1  19522  vieta1lem2  19523  aalioulem4  19547  aaliou3lem3  19556  abelthlem2  19640  abelthlem8  19647  abelthlem9  19648  sinhalfpilem  19666  efhalfpi  19671  cospi  19672  efipi  19673  sin2pi  19675  cos2pi  19676  ef2pi  19677  sin2pim  19685  cos2pim  19686  sinmpi  19687  cosmpi  19688  sinppi  19689  cosppi  19690  sincosq4sgn  19701  tangtx  19705  sincos4thpi  19713  sincos6thpi  19715  sincos3rdpi  19716  pige3  19717  abssinper  19718  efif1olem4  19739  efifo  19741  eff1o  19743  logneg  19773  logimul  19800  logneg2  19801  dvrelog  19816  logcnlem4  19824  dvlog  19830  dvlog2  19832  logtayl  19839  ang180lem1  19851  ang180lem2  19852  1cxp  19887  ecxp  19888  cxpsqr  19918  dvsqr  19952  root1eq1  19963  cxpeq  19965  1cubrlem  19969  1cubr  19970  dcubic2  19972  mcubic  19975  cubic2  19976  binom4  19978  dquartlem1  19979  dquartlem2  19980  dquart  19981  quart1lem  19983  quart1  19984  quartlem1  19985  asinsin  20020  asin1  20022  acos1  20023  atanlogsublem  20043  atanlogsub  20044  efiatan2  20045  2efiatan  20046  tanatan  20047  atanbnd  20054  atan1  20056  dvatan  20063  atantayl2  20066  leibpilem2  20069  leibpi  20070  log2cnv  20072  log2tlbnd  20073  log2ublem1  20074  log2ublem2  20075  log2ublem3  20076  log2ub  20077  birthday  20081  amgmlem  20116  emcllem5  20125  wilthlem2  20139  ftalem6  20147  basellem2  20151  basellem3  20152  basellem5  20154  basellem8  20157  cht1  20235  chp1  20237  1sgmprm  20270  ppiublem2  20274  ppiub  20275  chtublem  20282  chtub  20283  logfacbnd3  20294  bcp1ctr  20350  bclbnd  20351  bposlem1  20355  bposlem4  20358  bposlem6  20360  bposlem8  20362  bposlem9  20363  lgslem1  20367  lgsdir2lem1  20394  lgsdir2lem2  20395  lgsdir2lem3  20396  lgsdir2lem5  20398  lgs1  20409  lgseisenlem1  20420  lgseisenlem3  20422  lgsquadlem1  20425  lgsquadlem2  20426  lgsquad2lem2  20430  m1lgs  20433  2sqlem8  20443  2sqblem  20448  logdivsum  20514  mulog2sumlem2  20516  log2sumbnd  20525  selberglem1  20526  selberglem2  20527  pntrmax  20545  pntibndlem2  20572  pntibndlem3  20573  pntlemg  20579  pntlemr  20583  pntlemo  20588  ostth2lem3  20616  ostth2lem4  20617  smcnlem  21100  ipidsq  21116  dipcj  21120  dip0r  21123  nmlnoubi  21204  nmblolbii  21207  blocnilem  21212  ip1ilem  21234  ip2i  21236  ipdirilem  21237  ipasslem10  21247  ipasslem11  21248  siilem1  21259  hvmul0  21433  hvsubsub4i  21468  hvnegdii  21471  hvsubeq0i  21472  hvsubcan2i  21473  hvsubaddi  21475  hvsub0  21485  hisubcomi  21513  normlem0  21518  normlem1  21519  normlem2  21520  normlem3  21521  normlem9  21527  norm-ii-i  21546  norm3difi  21556  normpari  21563  polid2i  21566  polidi  21567  bcsiALT  21588  pjhthlem1  21800  chdmm3i  21888  chdmm4i  21889  chjidm  21929  chj4i  21932  chjjdiri  21933  spanunsni  21988  pjoml4i  22014  cmcm2i  22020  qlax4i  22057  qlax5i  22058  pjadjii  22101  pjmulii  22104  pjsubii  22105  pjssmii  22108  pjcji  22111  pjneli  22150  hoadd32i  22188  ho0subi  22205  hosubid1  22208  hosd2i  22233  hopncani  22234  hosubeq0i  22236  lnopeq0lem1  22415  lnopunilem1  22420  lnophmlem2  22427  nmbdoplbi  22434  nmcopexi  22437  lnfnmuli  22454  nmcfnexi  22461  nmoptri2i  22509  nmopcoadji  22511  golem1  22681  mdsl1i  22731  cvmdi  22734  mdslmd3i  22742  csmdsymi  22744  subfacp1lem1  22881  subfacp1lem5  22886  subfacval2  22889  subfaclim  22890  subfacval3  22891  cvxpcon  22944  cvxscon  22945  vdgr1c  23067  vdegp1ai  23079  vdegp1bi  23080  vdegp1ci  23081  sinccvglem  23176  4bc3eq4  23268  4bc2eq6  23269  frrlem5  23453  ax5seglem7  23737  axlowdimlem4  23747  axlowdimlem16  23759  bpoly0  23959  bpoly1  23960  bpolydiflem  23963  bpoly2  23966  bpoly3  23967  bpoly4  23968  fsumcube  23969  geme2  24441  nfwpr4c  24451  tolat  24452  fprodp1fi  24494  limfilnei  24727  1cat  24925  dualcat2  24950  isntr  25039  intset  25210  fnckle  25211  prdstotbnd  25684  prdsbnd2  25685  repwsmet  25724  rrnequiv  25725  reheibor  25729  mapfzcons  25959  mapfzcons1cl  25961  2rexfrabdioph  26043  3rexfrabdioph  26044  4rexfrabdioph  26045  6rexfrabdioph  26046  7rexfrabdioph  26047  rabdiophlem2  26049  diophren  26062  rabren3dioph  26064  pellexlem5  26084  pell1qr1  26122  rmspecfund  26160  jm2.17a  26213  jm2.17b  26214  jm2.27c  26266  jm2.27dlem5  26272  lmhmlnmsplit  26351  dsmmval2  26368  psgnunilem2  26584  psgnunilem4  26586  psgnpmtr  26599  lhe4.4ex1a  26712  expgrowthi  26716  expgrowth  26718  sec0  26919  dalem-cly  28549  pmodN  28728  cdleme0cp  29092  cdleme0cq  29093  cdleme1  29105  cdleme3d  29109  cdleme3h  29113  cdleme4  29116  cdleme5  29118  cdleme7a  29121  cdleme8  29128  cdleme9  29131  cdleme10  29132  cdleme11g  29143  cdleme15b  29153  cdleme21  29215  cdleme22e  29222  cdleme22eALTN  29223  cdleme23c  29229  cdleme25cv  29236  cdleme35b  29328  cdleme35c  29329  cdleme42a  29349  cdleme42d  29351  cdleme43aN  29367  cdlemeg46gfv  29408  cdlemk35  29790  dihjatcclem1  30297  lcdval2  30469  mapdpglem21  30571
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 1926  ax-ext 2234
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 1883  df-clab 2240  df-cleq 2246  df-clel 2249  df-nfc 2374  df-rex 2514  df-rab 2516  df-v 2729  df-dif 3081  df-un 3083  df-in 3085  df-ss 3089  df-nul 3363  df-if 3471  df-sn 3550  df-pr 3551  df-op 3553  df-uni 3728  df-br 3921  df-opab 3975  df-xp 4594  df-cnv 4596  df-dm 4598  df-rn 4599  df-res 4600  df-ima 4601  df-fv 4608  df-ov 5713
  Copyright terms: Public domain W3C validator