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

Theorem fveq1i 5732
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 5730 . 2  |-  ( F  =  G  ->  ( F `  A )  =  ( G `  A ) )
31, 2ax-mp 5 1  |-  ( F `
 A )  =  ( G `  A
)
Colors of variables: wff set class
Syntax hints:    = wceq 1653   ` cfv 5457
This theorem is referenced by:  fveq12i  5736  fvun2  5798  fvopab3ig  5806  fvsnun1  5931  fvsnun2  5932  fvpr1  5938  fvpr2  5939  fvpr1g  5940  fvpr2g  5941  fvtp1  5942  fvtp2  5943  fvtp3  5944  fvtp1g  5945  fvtp2g  5946  fvtp3g  5947  fvresex  5985  fveqf1o  6032  ov  6196  ovigg  6197  ovg  6215  curry1  6441  curry2  6444  tfr2a  6659  rdgsucmptf  6689  rdgsucmptnf  6690  frsucmpt  6698  frsucmptn  6699  seqomlem1  6710  seqomlem3  6712  seqomlem4  6713  seqom0g  6716  seqomsuc  6717  abianfplem  6718  unblem2  7363  inf3lemb  7583  inf3lemc  7584  trcl  7667  r10  7697  r1sucg  7698  r1limg  7700  infxpenc2  7908  aleph0  7952  alephlim  7953  alephsuc  7954  alephfplem1  7990  alephfplem2  7991  ackbij2lem3  8126  cfsmolem  8155  infpssrlem1  8188  infpssrlem2  8189  fin23lem34  8231  fin23lem35  8232  isf32lem6  8243  isf32lem7  8244  isf32lem8  8245  isf34lem5  8263  hsmexlem7  8308  axdclem2  8405  canthp1lem2  8533  wunex2  8618  wuncval2  8627  addpiord  8766  mulpiord  8767  addpqnq  8820  mulpqnq  8823  fseq1p1m1  11127  om2uz0i  11292  om2uzrdg  11301  uzrdg0i  11304  uzrdgsuci  11305  hashkf  11625  hashgval  11626  hashinf  11628  revs1  11802  cats1fv  11828  shftidt  11902  fsumss  12524  isumclim3  12548  isumsup2  12631  ruclem4  12838  ruclem6  12839  ruclem7  12840  sadc0  12971  sadcp1  12972  sadcaddlem  12974  sadaddlem  12983  smup0  12996  smupp1  12997  algr0  13068  algrp1  13070  ndxarg  13494  strfv2d  13504  xpsc0  13790  xpsc1  13791  funcoppc  14077  fthepi  14130  homadm  14200  homacd  14201  prdsidlem  14732  prdsinvlem  14931  cayleylem2  15116  gsumval3  15519  gsumzaddlem  15531  gsumzmhm  15538  pgpfaclem1  15644  rngidval  15671  lidlval  16270  rspval  16271  lidlnegcl  16290  lpival  16321  znf1o  16837  restcls  17250  restntr  17251  upxp  17660  cnmetdval  18810  remetdval  18825  qdensere2  18833  pcoptcl  19051  pcopt  19052  pcopt2  19053  pcorevlem  19056  ovolfsval  19372  ovollb2lem  19389  ovolunlem1a  19397  ovoliunlem1  19403  ovoliun2  19407  ovolscalem1  19414  ovolicc2lem4  19421  mblvol  19431  ioombl1lem4  19460  uniioovol  19476  uniioombllem3  19482  0pval  19566  limccnp  19783  limccnp2  19784  dvcnvrelem2  19907  itgsubstlem  19937  evl1val  19953  ply1remlem  20090  plyrem  20227  qaa  20245  abelth  20362  efif1olem4  20452  eflog  20479  logef  20481  logeftb  20483  dvrelog  20533  dvlog  20547  cxpcn3  20637  efrlim  20813  wilthlem3  20858  basellem8  20875  lgsqrlem1  21130  2wlklemA  21559  2wlklemB  21560  2wlklemC  21561  wlkntrllem2  21565  wlkntrllem3  21566  constr3lem4  21639  constr3lem5  21640  vdgr1c  21681  eupares  21702  eupap1  21703  vdegp1ai  21711  vdegp1bi  21712  avril1  21762  vafval  22087  smfval  22089  0vfval  22090  nmcvfval  22091  vsfval  22119  pjoc2i  22945  pjcji  23191  ho0val  23258  hoival  23263  adjbdlnb  23592  nmopcoadji  23609  opsqrlem2  23649  opsqrlem5  23652  hmopidmchi  23659  hmopidmpji  23660  pjinvari  23699  pjadj2coi  23712  pj3lem1  23714  funcnvmptOLD  24087  funcnvmpt  24088  cnre2csqlem  24313  zzsnm  24347  rrhcn  24385  qqhre  24391  coinflippv  24746  eflgam  24834  derangenlem  24862  kur14lem2  24898  kur14lem3  24899  kur14lem5  24901  kur14lem6  24902  txsconlem  24932  cvmliftlem4  24980  cvmliftlem5  24981  cbvprod  25246  fprodss  25279  fprodefsum  25303  iprodclim3  25318  trpredmintr  25514  trpred0  25519  wfrlem5  25547  frrlem5  25591  funpartfv  25795  fullfunfv  25797  axlowdimlem8  25893  axlowdimlem9  25894  axlowdimlem11  25896  axlowdimlem12  25897  axlowdimlem17  25902  ftc1cnnc  26293  neibastop2lem  26403  heiborlem4  26537  heiborlem6  26539  rabdiophlem2  26876  dnnumch1  27133  aomclem6  27148  mncn0  27335  aaitgo  27358  rngunsnply  27369  symggen  27402  cytpval  27519  fmul01  27700  fmuldfeq  27703  fmul01lt1lem1  27704  fmul01lt1lem2  27705  itgsin0pilem1  27734  stoweidlem3  27742  stoweidlem17  27756  stoweidlem47  27786  cdlemk13  31723  cdlemk14  31725  cdlemk15  31726  cdlemk21N  31744  cdlemk20  31745  cdlemk56w  31844  lcfrlem1  32414  hdmapfval  32702
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-rex 2713  df-uni 4018  df-br 4216  df-iota 5421  df-fv 5465
  Copyright terms: Public domain W3C validator