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

Theorem fveq1i 5542
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 5540 . 2  |-  ( F  =  G  ->  ( F `  A )  =  ( G `  A ) )
31, 2ax-mp 8 1  |-  ( F `
 A )  =  ( G `  A
)
Colors of variables: wff set class
Syntax hints:    = wceq 1632   ` cfv 5271
This theorem is referenced by:  fveq12i  5546  fvun2  5607  fvopab3ig  5615  fvsnun1  5731  fvsnun2  5732  fvpr1  5738  fvpr2  5739  fvtp1  5740  fvtp2  5741  fvtp3  5742  fvresex  5778  fveqf1o  5822  ov  5983  ovigg  5984  ovg  6002  curry1  6226  curry2  6229  tfr2a  6427  rdgsucmptf  6457  rdgsucmptnf  6458  frsucmpt  6466  frsucmptn  6467  seqomlem1  6478  seqomlem3  6480  seqomlem4  6481  seqom0g  6484  seqomsuc  6485  abianfplem  6486  unblem2  7126  inf3lemb  7342  inf3lemc  7343  trcl  7426  r10  7456  r1sucg  7457  r1limg  7459  infxpenc2  7665  aleph0  7709  alephlim  7710  alephsuc  7711  alephfplem1  7747  alephfplem2  7748  ackbij2lem3  7883  cfsmolem  7912  infpssrlem1  7945  infpssrlem2  7946  fin23lem34  7988  fin23lem35  7989  isf32lem6  8000  isf32lem7  8001  isf32lem8  8002  isf34lem5  8020  hsmexlem7  8065  axdclem2  8163  canthp1lem2  8291  wunex2  8376  wuncval2  8385  addpiord  8524  mulpiord  8525  addpqnq  8578  mulpqnq  8581  fseq1p1m1  10873  om2uz0i  11026  om2uzrdg  11035  uzrdg0i  11038  uzrdgsuci  11039  hashkf  11355  hashgval  11356  hashinf  11358  revs1  11499  cats1fv  11525  shftidt  11593  fsumss  12214  isumclim3  12238  isumsup2  12321  ruclem4  12528  ruclem6  12529  ruclem7  12530  sadc0  12661  sadcp1  12662  sadcaddlem  12664  sadaddlem  12673  smup0  12686  smupp1  12687  algr0  12758  algrp1  12760  ndxarg  13184  strfv2d  13194  xpsc0  13478  xpsc1  13479  funcoppc  13765  fthepi  13818  homadm  13888  homacd  13889  prdsidlem  14420  prdsinvlem  14619  cayleylem2  14804  gsumval3  15207  gsumzaddlem  15219  gsumzmhm  15226  pgpfaclem1  15332  rngidval  15359  lidlval  15962  rspval  15963  lidlnegcl  15982  lpival  16013  znf1o  16521  restcls  16927  restntr  16928  upxp  17333  cnmetdval  18296  remetdval  18311  qdensere2  18319  pcoptcl  18535  pcopt  18536  pcopt2  18537  pcorevlem  18540  ovolfsval  18846  ovollb2lem  18863  ovolunlem1a  18871  ovoliunlem1  18877  ovoliun2  18881  ovolscalem1  18888  ovolicc2lem4  18895  mblvol  18905  ioombl1lem4  18934  uniioovol  18950  uniioombllem3  18956  0pval  19042  limccnp  19257  limccnp2  19258  dvcnvrelem2  19381  itgsubstlem  19411  evl1val  19427  ply1remlem  19564  plyrem  19701  qaa  19719  abelth  19833  efif1olem4  19923  eflog  19949  logef  19951  logeftb  19953  dvrelog  20000  dvlog  20014  cxpcn3  20104  efrlim  20280  wilthlem3  20324  basellem8  20341  lgsqrlem1  20596  avril1  20852  vafval  21175  smfval  21177  0vfval  21178  nmcvfval  21179  vsfval  21207  pjoc2i  22033  pjcji  22279  ho0val  22346  hoival  22351  adjbdlnb  22680  nmopcoadji  22697  opsqrlem2  22737  opsqrlem5  22740  hmopidmchi  22747  hmopidmpji  22748  pjinvari  22787  pjadj2coi  22800  pj3lem1  22802  funcnvmptOLD  23249  funcnvmpt  23250  cnre2csqlem  23309  coinflippv  23699  dmgmseqn0  23711  derangenlem  23717  kur14lem2  23753  kur14lem3  23754  kur14lem5  23756  kur14lem6  23757  txsconlem  23786  cvmliftlem4  23834  cvmliftlem5  23835  vdgr1c  23911  eupares  23914  eupap1  23915  vdegp1ai  23923  vdegp1bi  23924  cbvcprod  24137  trpredmintr  24305  trpred0  24310  wfrlem5  24331  frrlem5  24356  funpartfv  24555  fullfunfv  24557  axlowdimlem8  24649  axlowdimlem9  24650  axlowdimlem11  24652  axlowdimlem12  24653  axlowdimlem17  24658  ftc1cnnc  25025  cbvprodi  25415  expmiz  25466  trooo  25497  trinv  25498  trnij  25718  valvze  25757  domval  25826  codval  25827  idval  25828  cmpval  25829  rdmob  25851  homib  25899  ismona  25912  issrc  25970  propsrc  25971  isntr  25976  cmp2morpcats  26064  cmp2morpgrp  26066  morexcmp  26070  cmpidmor2  26072  neibastop2lem  26412  heiborlem4  26641  heiborlem6  26643  rabdiophlem2  26986  dnnumch1  27244  aomclem6  27259  mncn0  27447  aaitgo  27470  rngunsnply  27481  symggen  27514  cytpval  27631  fmul01  27813  fmuldfeq  27816  fmul01lt1lem1  27817  fmul01lt1lem2  27818  itgsin0pilem1  27847  stoweidlem3  27855  stoweidlem17  27869  stoweidlem47  27899  wlkntrllem4  28348  wlkntrllem5  28349  constr3lem4  28393  constr3lem5  28394  cdlemk13  31663  cdlemk14  31665  cdlemk15  31666  cdlemk21N  31684  cdlemk20  31685  cdlemk56w  31784  lcfrlem1  32354  hdmapfval  32642
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-rex 2562  df-uni 3844  df-br 4040  df-iota 5235  df-fv 5279
  Copyright terms: Public domain W3C validator