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

Theorem fveq1i 5849
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 5847 . 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 1398   ` cfv 5570
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-rex 2810  df-uni 4236  df-br 4440  df-iota 5534  df-fv 5578
This theorem is referenced by:  fveq12i  5853  fvun2  5920  fvopab3ig  5928  fvsnun1  6082  fvsnun2  6083  fvpr1  6090  fvpr2  6091  fvpr1g  6092  fvpr2g  6093  fvtp1  6094  fvtp2  6095  fvtp3  6096  fvtp1g  6097  fvtp2g  6098  fvtp3g  6099  fveqf1o  6180  ov  6395  ovigg  6396  ovg  6414  fvresex  6746  curry1  6865  curry2  6868  suppsnop  6905  tfr2a  7056  rdgsucmptf  7086  rdgsucmptnf  7087  frsucmpt  7095  frsucmptn  7096  seqomlem1  7107  seqomlem3  7109  seqomlem4  7110  seqom0g  7113  seqomsuc  7114  unblem2  7765  inf3lemb  8033  inf3lemc  8034  trcl  8150  r10  8177  r1sucg  8178  r1limg  8180  infxpenc2  8390  infxpenc2OLD  8394  aleph0  8438  alephlim  8439  alephsuc  8440  alephfplem1  8476  alephfplem2  8477  ackbij2lem3  8612  cfsmolem  8641  infpssrlem1  8674  infpssrlem2  8675  fin23lem34  8717  fin23lem35  8718  isf32lem6  8729  isf32lem7  8730  isf32lem8  8731  isf34lem5  8749  hsmexlem7  8794  axdclem2  8891  canthp1lem2  9020  wunex2  9105  wuncval2  9114  addpiord  9251  mulpiord  9252  addpqnq  9305  mulpqnq  9308  fseq1p1m1  11756  om2uz0i  12043  om2uzrdg  12052  uzrdg0i  12055  uzrdgsuci  12056  hashkf  12392  hashgval  12393  hashinf  12395  revs1  12733  cats1fv  12818  shftidt  13000  cbvsum  13602  fsumss  13632  isumclim3  13659  isumsup2  13743  cbvprod  13807  fprodss  13840  iprodclim3  13878  fprodefsum  13915  ruclem4  14054  ruclem6  14055  ruclem7  14056  sadc0  14191  sadcp1  14192  sadcaddlem  14194  sadaddlem  14203  smup0  14216  smupp1  14217  algr0  14288  algrp1  14290  ndxarg  14739  strfv2d  14753  xpsc0  15052  xpsc1  15053  funcoppc  15366  fthepi  15419  homadm  15521  homacd  15522  prdsidlem  16154  prdsinvlem  16380  cayleylem2  16640  symggen  16697  pmtr3ncomlem1  16700  gsumval3OLD  17110  gsumval3  17113  gsumzaddlem  17136  gsumzaddlemOLD  17138  gsumzmhm  17158  gsumzmhmOLD  17159  pgpfaclem1  17330  ringidval  17353  lidlval  18036  rspval  18037  lidlnegcl  18059  lpival  18091  eqcoe1ply1eq  18537  evls1val  18555  evl1val  18563  znf1o  18766  mat1dimmul  19148  mdetralt  19280  mdetunilem7  19290  decpmatid  19441  pmatcollpwscmatlem1  19460  cpmidpmat  19544  chcoeffeq  19557  restcls  19852  restntr  19853  upxp  20293  cnmetdval  21447  remetdval  21463  qdensere2  21471  pcoptcl  21690  pcopt  21691  pcopt2  21692  pcorevlem  21695  ovolfsval  22051  ovollb2lem  22068  ovolunlem1a  22076  ovoliunlem1  22082  ovoliun2  22086  ovolscalem1  22093  ovolicc2lem4  22100  mblvol  22110  ioombl1lem4  22140  uniioovol  22157  uniioombllem3  22163  0pval  22247  limccnp  22464  limccnp2  22465  dvcnvrelem2  22588  itgsubstlem  22618  ply1remlem  22732  plyrem  22870  qaa  22888  abelth  23005  efif1olem4  23101  eflog  23133  logef  23138  logeftb  23140  dvrelog  23189  dvlog  23203  cxpcn3  23293  efrlim  23500  wilthlem3  23545  basellem8  23562  lgsqrlem1  23817  krippenlem  24271  colperpexlem1  24308  opphllem3  24325  lmiisolem  24365  axlowdimlem8  24457  axlowdimlem9  24458  axlowdimlem11  24460  axlowdimlem12  24461  axlowdimlem17  24466  2wlklemA  24761  2wlklemB  24762  2wlklemC  24763  wlkntrllem2  24767  wlkntrllem3  24768  constr3lem4  24852  constr3lem5  24853  wlkiswwlksur  24924  vdgr1c  25110  eupares  25180  eupap1  25181  vdegp1ai  25189  vdegp1bi  25190  avril1  25376  vafval  25697  smfval  25699  0vfval  25700  nmcvfval  25701  vsfval  25729  pjoc2i  26557  pjcji  26803  ho0val  26870  hoival  26875  adjbdlnb  27204  nmopcoadji  27221  opsqrlem2  27261  opsqrlem5  27264  hmopidmchi  27271  hmopidmpji  27272  pjinvari  27311  pjadj2coi  27324  pj3lem1  27326  funcnvmptOLD  27739  funcnvmpt  27740  cnre2csqlem  28130  zzsnm  28179  rrhcn  28215  qqhre  28235  oms0  28508  omsmon  28509  omssubaddlem  28510  omssubadd  28511  eulerpart  28588  fib0  28605  fib1  28606  fibp1  28607  coinflippv  28689  gsumnunsn  28760  eflgam  28854  derangenlem  28882  kur14lem2  28918  kur14lem3  28919  kur14lem5  28921  kur14lem6  28922  txsconlem  28952  cvmliftlem4  29000  cvmliftlem5  29001  trpredmintr  29557  trpred0  29562  wfrlem5  29590  frrlem5  29634  funpartfv  29826  fullfunfv  29828  ftc1cnnc  30332  neibastop2lem  30421  heiborlem4  30553  heiborlem6  30555  rabdiophlem2  30978  dnnumch1  31232  aomclem6  31247  mncn0  31332  aaitgo  31355  rngunsnply  31366  cytpval  31413  binomcxplemdvsum  31504  binomcxplemnotnn0  31505  binomcxp  31506  fmul01  31816  fmuldfeq  31819  fmul01lt1lem1  31820  fmul01lt1lem2  31821  lptioo2cn  31893  lptioo1cn  31894  limclner  31899  dvsinax  31950  fperdvper  31957  dvnmul  31982  dvnprodlem1  31985  dvnprodlem2  31986  dvnprodlem3  31987  itgsin0pilem1  31990  stoweidlem3  32027  stoweidlem17  32041  stoweidlem47  32071  fourierdlem42  32173  fourierdlem62  32193  fourierdlem80  32211  fourierdlem90  32221  fourierdlem92  32223  fourierdlem93  32224  fourierdlem103  32234  fourierdlem104  32235  fouriercnp  32251  rhmsubclem2  33168  rhmsubcALTVlem2  33187  ply1mulgsum  33263  lineval  33267  lincvalpr  33292  lindslinindimp2lem4  33335  zlmodzxzldeplem3  33376  zlmodzxzldeplem4  33377  cdlemk13  36994  cdlemk14  36996  cdlemk15  36997  cdlemk21N  37015  cdlemk20  37016  cdlemk56w  37115  lcfrlem1  37685  hdmapfval  37973
  Copyright terms: Public domain W3C validator