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

Theorem fveq1i 5720
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 5718 . 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 1652   ` cfv 5445
This theorem is referenced by:  fveq12i  5724  fvun2  5786  fvopab3ig  5794  fvsnun1  5919  fvsnun2  5920  fvpr1  5926  fvpr2  5927  fvpr1g  5928  fvpr2g  5929  fvtp1  5930  fvtp2  5931  fvtp3  5932  fvtp1g  5933  fvtp2g  5934  fvtp3g  5935  fvresex  5973  fveqf1o  6020  ov  6184  ovigg  6185  ovg  6203  curry1  6429  curry2  6432  tfr2a  6647  rdgsucmptf  6677  rdgsucmptnf  6678  frsucmpt  6686  frsucmptn  6687  seqomlem1  6698  seqomlem3  6700  seqomlem4  6701  seqom0g  6704  seqomsuc  6705  abianfplem  6706  unblem2  7351  inf3lemb  7569  inf3lemc  7570  trcl  7653  r10  7683  r1sucg  7684  r1limg  7686  infxpenc2  7892  aleph0  7936  alephlim  7937  alephsuc  7938  alephfplem1  7974  alephfplem2  7975  ackbij2lem3  8110  cfsmolem  8139  infpssrlem1  8172  infpssrlem2  8173  fin23lem34  8215  fin23lem35  8216  isf32lem6  8227  isf32lem7  8228  isf32lem8  8229  isf34lem5  8247  hsmexlem7  8292  axdclem2  8389  canthp1lem2  8517  wunex2  8602  wuncval2  8611  addpiord  8750  mulpiord  8751  addpqnq  8804  mulpqnq  8807  fseq1p1m1  11110  om2uz0i  11275  om2uzrdg  11284  uzrdg0i  11287  uzrdgsuci  11288  hashkf  11608  hashgval  11609  hashinf  11611  revs1  11785  cats1fv  11811  shftidt  11885  fsumss  12507  isumclim3  12531  isumsup2  12614  ruclem4  12821  ruclem6  12822  ruclem7  12823  sadc0  12954  sadcp1  12955  sadcaddlem  12957  sadaddlem  12966  smup0  12979  smupp1  12980  algr0  13051  algrp1  13053  ndxarg  13477  strfv2d  13487  xpsc0  13773  xpsc1  13774  funcoppc  14060  fthepi  14113  homadm  14183  homacd  14184  prdsidlem  14715  prdsinvlem  14914  cayleylem2  15099  gsumval3  15502  gsumzaddlem  15514  gsumzmhm  15521  pgpfaclem1  15627  rngidval  15654  lidlval  16253  rspval  16254  lidlnegcl  16273  lpival  16304  znf1o  16820  restcls  17233  restntr  17234  upxp  17643  cnmetdval  18793  remetdval  18808  qdensere2  18816  pcoptcl  19034  pcopt  19035  pcopt2  19036  pcorevlem  19039  ovolfsval  19355  ovollb2lem  19372  ovolunlem1a  19380  ovoliunlem1  19386  ovoliun2  19390  ovolscalem1  19397  ovolicc2lem4  19404  mblvol  19414  ioombl1lem4  19443  uniioovol  19459  uniioombllem3  19465  0pval  19551  limccnp  19766  limccnp2  19767  dvcnvrelem2  19890  itgsubstlem  19920  evl1val  19936  ply1remlem  20073  plyrem  20210  qaa  20228  abelth  20345  efif1olem4  20435  eflog  20462  logef  20464  logeftb  20466  dvrelog  20516  dvlog  20530  cxpcn3  20620  efrlim  20796  wilthlem3  20841  basellem8  20858  lgsqrlem1  21113  2wlklemA  21542  2wlklemB  21543  2wlklemC  21544  wlkntrllem2  21548  wlkntrllem3  21549  constr3lem4  21622  constr3lem5  21623  vdgr1c  21664  eupares  21685  eupap1  21686  vdegp1ai  21694  vdegp1bi  21695  avril1  21745  vafval  22070  smfval  22072  0vfval  22073  nmcvfval  22074  vsfval  22102  pjoc2i  22928  pjcji  23174  ho0val  23241  hoival  23246  adjbdlnb  23575  nmopcoadji  23592  opsqrlem2  23632  opsqrlem5  23635  hmopidmchi  23642  hmopidmpji  23643  pjinvari  23682  pjadj2coi  23695  pj3lem1  23697  funcnvmptOLD  24070  funcnvmpt  24071  cnre2csqlem  24296  zzsnm  24330  rrhcn  24368  qqhre  24374  coinflippv  24729  eflgam  24817  derangenlem  24845  kur14lem2  24881  kur14lem3  24882  kur14lem5  24884  kur14lem6  24885  txsconlem  24915  cvmliftlem4  24963  cvmliftlem5  24964  cbvprod  25230  fprodss  25263  fprodefsum  25287  iprodclim3  25302  trpredmintr  25489  trpred0  25494  wfrlem5  25515  frrlem5  25540  funpartfv  25740  fullfunfv  25742  axlowdimlem8  25836  axlowdimlem9  25837  axlowdimlem11  25839  axlowdimlem12  25840  axlowdimlem17  25845  ftc1cnnc  26225  neibastop2lem  26326  heiborlem4  26460  heiborlem6  26462  rabdiophlem2  26799  dnnumch1  27056  aomclem6  27071  mncn0  27259  aaitgo  27282  rngunsnply  27293  symggen  27326  cytpval  27443  fmul01  27624  fmuldfeq  27627  fmul01lt1lem1  27628  fmul01lt1lem2  27629  itgsin0pilem1  27658  stoweidlem3  27666  stoweidlem17  27680  stoweidlem47  27710  cdlemk13  31488  cdlemk14  31490  cdlemk15  31491  cdlemk21N  31509  cdlemk20  31510  cdlemk56w  31609  lcfrlem1  32179  hdmapfval  32467
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-rex 2703  df-uni 4008  df-br 4205  df-iota 5409  df-fv 5453
  Copyright terms: Public domain W3C validator