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

Theorem fveq1i 5867
Description: Equality inference for function value. (Contributed by NM, 2-Sep-2003.)
Hypothesis
Ref Expression
fveq1i.1  |-  F  =  G
Assertion
Ref Expression
fveq1i  |-  ( F `
 A )  =  ( G `  A
)

Proof of Theorem fveq1i
StepHypRef Expression
1 fveq1i.1 . 2  |-  F  =  G
2 fveq1 5865 . 2  |-  ( F  =  G  ->  ( F `  A )  =  ( G `  A ) )
31, 2ax-mp 5 1  |-  ( F `
 A )  =  ( G `  A
)
Colors of variables: wff setvar class
Syntax hints:    = wceq 1379   ` cfv 5588
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-rex 2820  df-uni 4246  df-br 4448  df-iota 5551  df-fv 5596
This theorem is referenced by:  fveq12i  5871  fvun2  5939  fvopab3ig  5947  fvsnun1  6096  fvsnun2  6097  fvpr1  6104  fvpr2  6105  fvpr1g  6106  fvpr2g  6107  fvtp1  6108  fvtp2  6109  fvtp3  6110  fvtp1g  6111  fvtp2g  6112  fvtp3g  6113  fveqf1o  6193  ov  6406  ovigg  6407  ovg  6425  fvresex  6757  curry1  6875  curry2  6878  suppsnop  6915  tfr2a  7064  rdgsucmptf  7094  rdgsucmptnf  7095  frsucmpt  7103  frsucmptn  7104  seqomlem1  7115  seqomlem3  7117  seqomlem4  7118  seqom0g  7121  seqomsuc  7122  unblem2  7773  inf3lemb  8042  inf3lemc  8043  trcl  8159  r10  8186  r1sucg  8187  r1limg  8189  infxpenc2  8399  infxpenc2OLD  8403  aleph0  8447  alephlim  8448  alephsuc  8449  alephfplem1  8485  alephfplem2  8486  ackbij2lem3  8621  cfsmolem  8650  infpssrlem1  8683  infpssrlem2  8684  fin23lem34  8726  fin23lem35  8727  isf32lem6  8738  isf32lem7  8739  isf32lem8  8740  isf34lem5  8758  hsmexlem7  8803  axdclem2  8900  canthp1lem2  9031  wunex2  9116  wuncval2  9125  addpiord  9262  mulpiord  9263  addpqnq  9316  mulpqnq  9319  fseq1p1m1  11752  om2uz0i  12026  om2uzrdg  12035  uzrdg0i  12038  uzrdgsuci  12039  hashkf  12375  hashgval  12376  hashinf  12378  revs1  12702  cats1fv  12787  shftidt  12878  cbvsum  13480  fsumss  13510  isumclim3  13537  isumsup2  13621  ruclem4  13828  ruclem6  13829  ruclem7  13830  sadc0  13963  sadcp1  13964  sadcaddlem  13966  sadaddlem  13975  smup0  13988  smupp1  13989  algr0  14060  algrp1  14062  ndxarg  14510  strfv2d  14522  xpsc0  14815  xpsc1  14816  funcoppc  15102  fthepi  15155  homadm  15225  homacd  15226  prdsidlem  15771  prdsinvlem  15988  cayleylem2  16243  symggen  16301  pmtr3ncomlem1  16304  gsumval3OLD  16711  gsumval3  16714  gsumzaddlem  16737  gsumzaddlemOLD  16739  gsumzmhm  16760  gsumzmhmOLD  16761  pgpfaclem1  16934  rngidval  16957  lidlval  17638  rspval  17639  lidlnegcl  17661  lpival  17692  eqcoe1ply1eq  18138  evls1val  18156  evl1val  18164  znf1o  18385  mat1dimmul  18773  mdetralt  18905  mdetunilem7  18915  decpmatid  19066  pmatcollpwscmatlem1  19085  cpmidpmat  19169  chcoeffeq  19182  restcls  19476  restntr  19477  upxp  19887  cnmetdval  21041  remetdval  21057  qdensere2  21065  pcoptcl  21284  pcopt  21285  pcopt2  21286  pcorevlem  21289  ovolfsval  21645  ovollb2lem  21662  ovolunlem1a  21670  ovoliunlem1  21676  ovoliun2  21680  ovolscalem1  21687  ovolicc2lem4  21694  mblvol  21704  ioombl1lem4  21734  uniioovol  21751  uniioombllem3  21757  0pval  21841  limccnp  22058  limccnp2  22059  dvcnvrelem2  22182  itgsubstlem  22212  ply1remlem  22326  plyrem  22463  qaa  22481  abelth  22598  efif1olem4  22693  eflog  22720  logef  22722  logeftb  22724  dvrelog  22774  dvlog  22788  cxpcn3  22878  efrlim  23055  wilthlem3  23100  basellem8  23117  lgsqrlem1  23372  krippenlem  23803  colperpexlem1  23837  lmiisolem  23866  axlowdimlem8  23956  axlowdimlem9  23957  axlowdimlem11  23959  axlowdimlem12  23960  axlowdimlem17  23965  2wlklemA  24260  2wlklemB  24261  2wlklemC  24262  wlkntrllem2  24266  wlkntrllem3  24267  constr3lem4  24351  constr3lem5  24352  wlkiswwlksur  24423  vdgr1c  24609  eupares  24679  eupap1  24680  vdegp1ai  24688  vdegp1bi  24689  avril1  24875  vafval  25200  smfval  25202  0vfval  25203  nmcvfval  25204  vsfval  25232  pjoc2i  26060  pjcji  26306  ho0val  26373  hoival  26378  adjbdlnb  26707  nmopcoadji  26724  opsqrlem2  26764  opsqrlem5  26767  hmopidmchi  26774  hmopidmpji  26775  pjinvari  26814  pjadj2coi  26827  pj3lem1  26829  funcnvmptOLD  27209  funcnvmpt  27210  cnre2csqlem  27556  zzsnm  27605  zzsnmOLD  27606  rrhcn  27642  qqhre  27662  oms0  27934  omsmon  27935  eulerpart  27989  fib0  28006  fib1  28007  fibp1  28008  coinflippv  28090  gsumnunsn  28161  eflgam  28255  derangenlem  28283  kur14lem2  28319  kur14lem3  28320  kur14lem5  28322  kur14lem6  28323  txsconlem  28353  cvmliftlem4  28401  cvmliftlem5  28402  cbvprod  28652  fprodss  28685  fprodefsum  28709  iprodclim3  28724  trpredmintr  28919  trpred0  28924  wfrlem5  28952  frrlem5  28996  funpartfv  29200  fullfunfv  29202  ftc1cnnc  29694  neibastop2lem  29809  heiborlem4  29941  heiborlem6  29943  rabdiophlem2  30367  dnnumch1  30622  aomclem6  30637  mncn0  30721  aaitgo  30744  rngunsnply  30755  cytpval  30802  fmul01  31158  fmuldfeq  31161  fmul01lt1lem1  31162  fmul01lt1lem2  31163  lptioo2cn  31215  lptioo1cn  31216  limclner  31221  icocncflimc  31256  dvsinax  31269  fperdvper  31276  itgsin0pilem1  31295  stoweidlem3  31331  stoweidlem17  31345  stoweidlem47  31375  fourierdlem42  31477  fourierdlem62  31497  fourierdlem80  31515  fourierdlem90  31525  fourierdlem92  31527  fourierdlem93  31528  fourierdlem103  31538  fourierdlem104  31539  fouriercnp  31555  ply1mulgsum  32089  lineval  32093  lincvalpr  32118  lindslinindimp2lem4  32161  zlmodzxzldeplem3  32202  zlmodzxzldeplem4  32203  cdlemk13  35666  cdlemk14  35668  cdlemk15  35669  cdlemk21N  35687  cdlemk20  35688  cdlemk56w  35787  lcfrlem1  36357  hdmapfval  36645
  Copyright terms: Public domain W3C validator