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

Theorem fveq1i 5526
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 5524 . 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 1623   ` cfv 5255
This theorem is referenced by:  fveq12i  5530  fvun2  5591  fvopab3ig  5599  fvsnun1  5715  fvsnun2  5716  fvpr1  5722  fvpr2  5723  fvtp1  5724  fvtp2  5725  fvtp3  5726  fvresex  5762  fveqf1o  5806  ov  5967  ovigg  5968  ovg  5986  curry1  6210  curry2  6213  tfr2a  6411  rdgsucmptf  6441  rdgsucmptnf  6442  frsucmpt  6450  frsucmptn  6451  seqomlem1  6462  seqomlem3  6464  seqomlem4  6465  seqom0g  6468  seqomsuc  6469  abianfplem  6470  unblem2  7110  inf3lemb  7326  inf3lemc  7327  trcl  7410  r10  7440  r1sucg  7441  r1limg  7443  infxpenc2  7649  aleph0  7693  alephlim  7694  alephsuc  7695  alephfplem1  7731  alephfplem2  7732  ackbij2lem3  7867  cfsmolem  7896  infpssrlem1  7929  infpssrlem2  7930  fin23lem34  7972  fin23lem35  7973  isf32lem6  7984  isf32lem7  7985  isf32lem8  7986  isf34lem5  8004  hsmexlem7  8049  axdclem2  8147  canthp1lem2  8275  wunex2  8360  wuncval2  8369  addpiord  8508  mulpiord  8509  addpqnq  8562  mulpqnq  8565  fseq1p1m1  10857  om2uz0i  11010  om2uzrdg  11019  uzrdg0i  11022  uzrdgsuci  11023  hashkf  11339  hashgval  11340  hashinf  11342  revs1  11483  cats1fv  11509  shftidt  11577  fsumss  12198  isumclim3  12222  isumsup2  12305  ruclem4  12512  ruclem6  12513  ruclem7  12514  sadc0  12645  sadcp1  12646  sadcaddlem  12648  sadaddlem  12657  smup0  12670  smupp1  12671  algr0  12742  algrp1  12744  ndxarg  13168  strfv2d  13178  xpsc0  13462  xpsc1  13463  funcoppc  13749  fthepi  13802  homadm  13872  homacd  13873  prdsidlem  14404  prdsinvlem  14603  cayleylem2  14788  gsumval3  15191  gsumzaddlem  15203  gsumzmhm  15210  pgpfaclem1  15316  rngidval  15343  lidlval  15946  rspval  15947  lidlnegcl  15966  lpival  15997  znf1o  16505  restcls  16911  restntr  16912  upxp  17317  cnmetdval  18280  remetdval  18295  qdensere2  18303  pcoptcl  18519  pcopt  18520  pcopt2  18521  pcorevlem  18524  ovolfsval  18830  ovollb2lem  18847  ovolunlem1a  18855  ovoliunlem1  18861  ovoliun2  18865  ovolscalem1  18872  ovolicc2lem4  18879  mblvol  18889  ioombl1lem4  18918  uniioovol  18934  uniioombllem3  18940  0pval  19026  limccnp  19241  limccnp2  19242  dvcnvrelem2  19365  itgsubstlem  19395  evl1val  19411  ply1remlem  19548  plyrem  19685  qaa  19703  abelth  19817  efif1olem4  19907  eflog  19933  logef  19935  logeftb  19937  dvrelog  19984  dvlog  19998  cxpcn3  20088  efrlim  20264  wilthlem3  20308  basellem8  20325  lgsqrlem1  20580  avril1  20836  vafval  21159  smfval  21161  0vfval  21162  nmcvfval  21163  vsfval  21191  pjoc2i  22017  pjcji  22263  ho0val  22330  hoival  22335  adjbdlnb  22664  nmopcoadji  22681  opsqrlem2  22721  opsqrlem5  22724  hmopidmchi  22731  hmopidmpji  22732  pjinvari  22771  pjadj2coi  22784  pj3lem1  22786  funcnvmptOLD  23234  funcnvmpt  23235  cnre2csqlem  23294  coinflippv  23684  dmgmseqn0  23696  derangenlem  23702  kur14lem2  23738  kur14lem3  23739  kur14lem5  23741  kur14lem6  23742  txsconlem  23771  cvmliftlem4  23819  cvmliftlem5  23820  vdgr1c  23896  eupares  23899  eupap1  23900  vdegp1ai  23908  vdegp1bi  23909  trpredmintr  24234  trpred0  24239  wfrlem5  24260  frrlem5  24285  funpartfv  24483  fullfunfv  24485  axlowdimlem8  24577  axlowdimlem9  24578  axlowdimlem11  24580  axlowdimlem12  24581  axlowdimlem17  24586  cbvprodi  25312  expmiz  25363  trooo  25394  trinv  25395  trnij  25615  valvze  25654  domval  25723  codval  25724  idval  25725  cmpval  25726  rdmob  25748  homib  25796  ismona  25809  issrc  25867  propsrc  25868  isntr  25873  cmp2morpcats  25961  cmp2morpgrp  25963  morexcmp  25967  cmpidmor2  25969  neibastop2lem  26309  heiborlem4  26538  heiborlem6  26540  rabdiophlem2  26883  dnnumch1  27141  aomclem6  27156  mncn0  27344  aaitgo  27367  rngunsnply  27378  symggen  27411  cytpval  27528  fmul01  27710  fmuldfeq  27713  fmul01lt1lem1  27714  fmul01lt1lem2  27715  itgsin0pilem1  27744  stoweidlem3  27752  stoweidlem17  27766  stoweidlem47  27796  cdlemk13  31041  cdlemk14  31043  cdlemk15  31044  cdlemk21N  31062  cdlemk20  31063  cdlemk56w  31162  lcfrlem1  31732  hdmapfval  32020
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-rex 2549  df-uni 3828  df-br 4024  df-iota 5219  df-fv 5263
  Copyright terms: Public domain W3C validator