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

Theorem oveq2i 5803
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 5800 . 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 5792
This theorem is referenced by:  caov32  5981  caov4  5985  caov42  5987  seqomsuc  6437  oa1suc  6498  om1  6508  oe1  6510  oawordeulem  6520  oeoalem  6562  nnm1  6614  nnm2  6615  nneob  6618  omopthlem1  6621  mapsnconst  6781  mapsncnv  6782  map2xp  6999  cantnflt  7341  cnfcom2  7373  infxpenc  7613  infxpenc2  7617  ackbij1lem5  7818  alephom  8175  pwxpndom2  8255  adderpqlem  8546  addassnq  8550  mulcanenq  8552  distrnq  8553  ltanq  8563  ltexnq  8567  halfnq  8568  ltrnq  8571  archnq  8572  addclprlem2  8609  prlem934  8625  prlem936  8639  addcmpblnr  8662  mulcmpblnrlem  8663  ltsrpr  8667  m1p1sr  8682  m1m1sr  8683  0idsr  8687  1idsr  8688  00sr  8689  pn0sr  8691  recexsrlem  8693  mulgt0sr  8695  sqgt0sr  8696  mulresr  8729  axmulcom  8745  axmulass  8747  axdistr  8748  axi2m1  8749  ax1rid  8751  axcnre  8754  mul02lem1  8956  addid1  8960  add42i  9000  negid  9062  negsub  9063  subneg  9064  negsubdii  9099  muleqadd  9380  crne0  9707  2p2e4  9810  3p2e5  9823  3p3e6  9824  4p2e6  9825  4p3e7  9826  4p4e8  9827  5p2e7  9828  5p3e8  9829  5p4e9  9830  5p5e10  9831  6p2e8  9832  6p3e9  9833  6p4e10  9834  7p2e9  9835  7p3e10  9836  8p2e10  9837  3t3e9  9841  8th4div3  9903  halfpm6th  9904  addltmul  9915  nneo  10063  zeo  10065  numsuc  10104  numltc  10112  numsucc  10118  numma  10123  nummul1c  10128  6p5lem  10141  4t3lem  10163  decbin2  10196  xmulmnf1  10563  fztp  10808  fzprval  10811  fztpval  10812  fzshftral  10836  fzo01  10880  quoremz  10926  quoremnn0  10928  intfrac2  10929  intfracq  10930  sqval  11130  sqrecii  11153  cu2  11168  i3  11171  i4  11172  binom2i  11179  binom3  11189  crreczi  11193  nn0opthlem1  11250  facp1  11260  faclbnd  11270  faclbnd2  11271  faclbnd4lem1  11273  faclbnd4lem4  11276  bcn1  11292  bcn2  11298  hashgadd  11326  hashxplem  11351  hashmap  11353  hashfun  11355  hashbclem  11356  fz1isolem  11365  ccatlid  11400  ccatrid  11401  eqs1  11413  wrdeqs1cat  11441  cats1un  11442  cats1fvn  11474  cats1cat  11477  swrds2  11526  reim0  11569  cji  11610  sqrm1  11727  absi  11737  rddif  11790  iseraltlem2  12121  iseralt  12123  fsump1i  12198  fsummulc2  12212  arisum2  12282  geoihalfsum  12301  mertenslem1  12303  mertens  12305  ef0lem  12323  ege2le3  12334  eft0val  12355  ef4p  12356  efgt1p2  12357  efgt1p  12358  tanval2  12376  efival  12395  ef01bndlem  12427  sin01bnd  12428  cos01bnd  12429  cos1bnd  12430  cos2bnd  12431  rpnnen2lem11  12466  sqr2irrlem  12489  odd2np1lem  12549  odd2np1  12550  oddp1even  12552  divalglem5  12559  divalglem6  12560  bits0  12582  0bits  12593  bitsinv1lem  12595  gcdaddmlem  12670  3prm  12738  phiprm  12808  eulerthlem2  12813  prmdiv  12816  opoe  12827  pythagtriplem12  12842  pythagtriplem14  12844  pcmpt  12903  pcfac  12910  prmpwdvds  12914  pockthi  12917  prmreclem2  12927  prmreclem6  12931  4sqlem5  12952  4sqlem13  12967  modxai  13046  mod2xnegi  13049  gcdi  13051  decexp2  13053  numexpp1  13056  numexp2x  13057  decsplit0b  13058  decsplit1  13060  decsplit  13061  2exp6  13064  2exp16  13066  prmlem0  13070  139prm  13088  163prm  13089  317prm  13090  631prm  13091  1259lem1  13092  1259lem3  13094  1259lem4  13095  1259lem5  13096  1259prm  13097  2503lem1  13098  2503lem2  13099  2503lem3  13100  2503prm  13101  4001lem1  13102  4001lem2  13103  4001lem3  13104  4001lem4  13105  ressinbas  13167  rescfth  13774  xpccatid  13925  oduval  14197  oppgmnd  14790  lsmmod2  14948  efgi0  14992  efgi1  14993  efginvrel2  14999  efgsval2  15005  efgsp1  15009  efgredleme  15015  efgredlemc  15017  efgcpbllemb  15027  frgpnabllem1  15124  lt6abl  15144  gsumsn  15183  gsum2d  15186  pwsgsum  15193  dprd0  15229  dprdf1  15231  dprd2da  15240  ablfac1lem  15266  pgpfac1lem3  15275  pgpfaclem1  15279  opprrng  15376  mulgass3  15382  ply1assa  16241  ply1coe  16331  zlmval  16433  znbas  16460  znzrh2  16462  restin  16860  imacmp  17087  concompcon  17121  uptx  17282  cnpflf2  17658  tmdgsum2  17742  tsmsres  17789  tsmsf1o  17790  tsmsmhm  17791  prdsxmet  17896  resspwsds  17899  prdsxmslem2  18038  metdcn2  18307  metdcn  18308  metdscn2  18324  iimulcn  18399  icchmeo  18402  xrhmeo  18407  cnrehmeo  18414  cnheiborlem  18415  evth  18420  evth2  18421  lebnumlem2  18423  reparphti  18458  pcoass  18485  pi1xfrcnv  18518  ipcau2  18627  minveclem4  18759  pjthlem1  18764  ovolunlem1a  18818  unmbl  18858  uniioombl  18907  iblitg  19086  dfitg  19087  itg0  19097  iblcnlem1  19105  itgcnlem  19107  itgabs  19152  limcdif  19189  limccnp  19204  limccnp2  19205  dvexp  19265  dvmptid  19269  dvmptc  19270  dvmptfsum  19285  dveflem  19289  dvsincos  19291  mvth  19302  dvlipcn  19304  dvivthlem1  19318  dvfsumle  19331  dvfsumlem2  19337  itgsubst  19359  evlsval  19366  mpff  19388  tdeglem4  19409  tdeglem2  19410  plypf1  19557  plymullem1  19559  coesub  19601  dgrmulc  19615  fta1lem  19650  vieta1lem1  19653  vieta1lem2  19654  aalioulem4  19678  aaliou3lem3  19687  abelthlem2  19771  abelthlem8  19778  abelthlem9  19779  sinhalfpilem  19797  efhalfpi  19802  cospi  19803  efipi  19804  sin2pi  19806  cos2pi  19807  ef2pi  19808  sin2pim  19816  cos2pim  19817  sinmpi  19818  cosmpi  19819  sinppi  19820  cosppi  19821  sincosq4sgn  19832  tangtx  19836  sincos4thpi  19844  sincos6thpi  19846  sincos3rdpi  19847  pige3  19848  abssinper  19849  efif1olem4  19870  efifo  19872  eff1o  19874  logneg  19904  logimul  19931  logneg2  19932  dvrelog  19947  logcnlem4  19955  dvlog  19961  dvlog2  19963  logtayl  19970  1cxp  19982  ecxp  19983  cxpsqr  20013  dvsqr  20047  root1eq1  20058  cxpeq  20060  ang180lem1  20070  ang180lem2  20071  1cubrlem  20100  1cubr  20101  dcubic2  20103  mcubic  20106  cubic2  20107  binom4  20109  dquartlem1  20110  dquartlem2  20111  dquart  20112  quart1lem  20114  quart1  20115  quartlem1  20116  asinsin  20151  asin1  20153  acos1  20154  atanlogsublem  20174  atanlogsub  20175  efiatan2  20176  2efiatan  20177  tanatan  20178  atanbnd  20185  atan1  20187  dvatan  20194  atantayl2  20197  leibpilem2  20200  leibpi  20201  log2cnv  20203  log2tlbnd  20204  log2ublem1  20205  log2ublem2  20206  log2ublem3  20207  log2ub  20208  birthday  20212  amgmlem  20247  emcllem5  20256  wilthlem2  20270  ftalem6  20278  basellem2  20282  basellem3  20283  basellem5  20285  basellem8  20288  cht1  20366  chp1  20368  1sgmprm  20401  ppiublem2  20405  ppiub  20406  chtublem  20413  chtub  20414  logfacbnd3  20425  bcp1ctr  20481  bclbnd  20482  bposlem1  20486  bposlem4  20489  bposlem6  20491  bposlem8  20493  bposlem9  20494  lgslem1  20498  lgsdir2lem1  20525  lgsdir2lem2  20526  lgsdir2lem3  20527  lgsdir2lem5  20529  lgs1  20540  lgseisenlem1  20551  lgseisenlem3  20553  lgsquadlem1  20556  lgsquadlem2  20557  lgsquad2lem2  20561  m1lgs  20564  2sqlem8  20574  2sqblem  20579  logdivsum  20645  mulog2sumlem2  20647  log2sumbnd  20656  selberglem1  20657  selberglem2  20658  pntrmax  20676  pntibndlem2  20703  pntibndlem3  20704  pntlemg  20710  pntlemr  20714  pntlemo  20719  ostth2lem3  20747  ostth2lem4  20748  smcnlem  21231  ipidsq  21247  dipcj  21251  dip0r  21254  nmlnoubi  21335  nmblolbii  21338  blocnilem  21343  ip1ilem  21365  ip2i  21367  ipdirilem  21368  ipasslem10  21378  ipasslem11  21379  siilem1  21390  hvmul0  21564  hvsubsub4i  21599  hvnegdii  21602  hvsubeq0i  21603  hvsubcan2i  21604  hvsubaddi  21606  hvsub0  21616  hisubcomi  21644  normlem0  21649  normlem1  21650  normlem2  21651  normlem3  21652  normlem9  21658  norm-ii-i  21677  norm3difi  21687  normpari  21694  polid2i  21697  polidi  21698  bcsiALT  21719  pjhthlem1  21931  chdmm3i  22019  chdmm4i  22020  chjidm  22060  chj4i  22063  chjjdiri  22064  spanunsni  22119  pjoml4i  22127  cmcm2i  22133  qlax4i  22170  qlax5i  22171  pjadjii  22214  pjmulii  22217  pjsubii  22218  pjssmii  22221  pjcji  22224  pjneli  22263  hoadd32i  22319  ho0subi  22336  hosubid1  22339  hosd2i  22364  hopncani  22365  hosubeq0i  22367  lnopeq0lem1  22546  lnopunilem1  22551  lnophmlem2  22558  nmbdoplbi  22565  nmcopexi  22568  lnfnmuli  22585  nmcfnexi  22592  nmoptri2i  22640  nmopcoadji  22642  golem1  22812  mdsl1i  22862  cvmdi  22865  mdslmd3i  22873  csmdsymi  22875  ballotlem2  23009  ballotth  23058  subfacp1lem1  23083  subfacp1lem5  23088  subfacval2  23091  subfaclim  23092  subfacval3  23093  cvxpcon  23146  cvxscon  23147  vdgr1c  23269  vdegp1ai  23281  vdegp1bi  23282  vdegp1ci  23283  sinccvglem  23378  4bc3eq4  23470  4bc2eq6  23471  frrlem5  23655  ax5seglem7  23939  axlowdimlem4  23949  axlowdimlem16  23961  bpoly0  24161  bpoly1  24162  bpolydiflem  24165  bpoly2  24168  bpoly3  24169  bpoly4  24170  fsumcube  24171  geme2  24643  nfwpr4c  24653  tolat  24654  fprodp1fi  24696  limfilnei  24929  1cat  25127  dualcat2  25152  isntr  25241  intset  25412  fnckle  25413  prdstotbnd  25886  prdsbnd2  25887  repwsmet  25926  rrnequiv  25927  reheibor  25931  mapfzcons  26161  mapfzcons1cl  26163  2rexfrabdioph  26245  3rexfrabdioph  26246  4rexfrabdioph  26247  6rexfrabdioph  26248  7rexfrabdioph  26249  rabdiophlem2  26251  diophren  26264  rabren3dioph  26266  pellexlem5  26286  pell1qr1  26324  rmspecfund  26362  jm2.17a  26415  jm2.17b  26416  jm2.27c  26468  jm2.27dlem5  26474  lmhmlnmsplit  26553  dsmmval2  26570  psgnunilem2  26786  psgnunilem4  26788  psgnpmtr  26801  lhe4.4ex1a  26914  expgrowthi  26918  expgrowth  26920  refsumcn  27070  m1expeven  27094  dvcosre  27110  itgsin0pilem1  27113  itgsinexplem1  27117  stoweidlem13  27131  wallispilem4  27186  wallispi2lem1  27189  wallispi2lem2  27190  stirlinglem1  27192  sec0  27363  dalem-cly  29110  pmodN  29289  cdleme0cp  29653  cdleme0cq  29654  cdleme1  29666  cdleme3d  29670  cdleme3h  29674  cdleme4  29677  cdleme5  29679  cdleme7a  29682  cdleme8  29689  cdleme9  29692  cdleme10  29693  cdleme11g  29704  cdleme15b  29714  cdleme21  29776  cdleme22e  29783  cdleme22eALTN  29784  cdleme23c  29790  cdleme25cv  29797  cdleme35b  29889  cdleme35c  29890  cdleme42a  29910  cdleme42d  29912  cdleme43aN  29928  cdlemeg46gfv  29969  cdlemk35  30351  dihjatcclem1  30858  lcdval2  31030  mapdpglem21  31132
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 2239
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 2245  df-cleq 2251  df-clel 2254  df-nfc 2383  df-rex 2524  df-rab 2527  df-v 2765  df-dif 3130  df-un 3132  df-in 3134  df-ss 3141  df-nul 3431  df-if 3540  df-sn 3620  df-pr 3621  df-op 3623  df-uni 3802  df-br 3998  df-opab 4052  df-xp 4675  df-cnv 4677  df-dm 4679  df-rn 4680  df-res 4681  df-ima 4682  df-fv 4689  df-ov 5795
  Copyright terms: Public domain W3C validator