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

Theorem fveq1i 5696
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 5694 . 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 1649   ` cfv 5421
This theorem is referenced by:  fveq12i  5700  fvun2  5762  fvopab3ig  5770  fvsnun1  5895  fvsnun2  5896  fvpr1  5902  fvpr2  5903  fvpr1g  5904  fvpr2g  5905  fvtp1  5906  fvtp2  5907  fvtp3  5908  fvtp1g  5909  fvtp2g  5910  fvtp3g  5911  fvresex  5949  fveqf1o  5996  ov  6160  ovigg  6161  ovg  6179  curry1  6405  curry2  6408  tfr2a  6623  rdgsucmptf  6653  rdgsucmptnf  6654  frsucmpt  6662  frsucmptn  6663  seqomlem1  6674  seqomlem3  6676  seqomlem4  6677  seqom0g  6680  seqomsuc  6681  abianfplem  6682  unblem2  7327  inf3lemb  7544  inf3lemc  7545  trcl  7628  r10  7658  r1sucg  7659  r1limg  7661  infxpenc2  7867  aleph0  7911  alephlim  7912  alephsuc  7913  alephfplem1  7949  alephfplem2  7950  ackbij2lem3  8085  cfsmolem  8114  infpssrlem1  8147  infpssrlem2  8148  fin23lem34  8190  fin23lem35  8191  isf32lem6  8202  isf32lem7  8203  isf32lem8  8204  isf34lem5  8222  hsmexlem7  8267  axdclem2  8364  canthp1lem2  8492  wunex2  8577  wuncval2  8586  addpiord  8725  mulpiord  8726  addpqnq  8779  mulpqnq  8782  fseq1p1m1  11085  om2uz0i  11250  om2uzrdg  11259  uzrdg0i  11262  uzrdgsuci  11263  hashkf  11583  hashgval  11584  hashinf  11586  revs1  11760  cats1fv  11786  shftidt  11860  fsumss  12482  isumclim3  12506  isumsup2  12589  ruclem4  12796  ruclem6  12797  ruclem7  12798  sadc0  12929  sadcp1  12930  sadcaddlem  12932  sadaddlem  12941  smup0  12954  smupp1  12955  algr0  13026  algrp1  13028  ndxarg  13452  strfv2d  13462  xpsc0  13748  xpsc1  13749  funcoppc  14035  fthepi  14088  homadm  14158  homacd  14159  prdsidlem  14690  prdsinvlem  14889  cayleylem2  15074  gsumval3  15477  gsumzaddlem  15489  gsumzmhm  15496  pgpfaclem1  15602  rngidval  15629  lidlval  16228  rspval  16229  lidlnegcl  16248  lpival  16279  znf1o  16795  restcls  17207  restntr  17208  upxp  17616  cnmetdval  18766  remetdval  18781  qdensere2  18789  pcoptcl  19007  pcopt  19008  pcopt2  19009  pcorevlem  19012  ovolfsval  19328  ovollb2lem  19345  ovolunlem1a  19353  ovoliunlem1  19359  ovoliun2  19363  ovolscalem1  19370  ovolicc2lem4  19377  mblvol  19387  ioombl1lem4  19416  uniioovol  19432  uniioombllem3  19438  0pval  19524  limccnp  19739  limccnp2  19740  dvcnvrelem2  19863  itgsubstlem  19893  evl1val  19909  ply1remlem  20046  plyrem  20183  qaa  20201  abelth  20318  efif1olem4  20408  eflog  20435  logef  20437  logeftb  20439  dvrelog  20489  dvlog  20503  cxpcn3  20593  efrlim  20769  wilthlem3  20814  basellem8  20831  lgsqrlem1  21086  2wlklemA  21515  2wlklemB  21516  2wlklemC  21517  wlkntrllem2  21521  wlkntrllem3  21522  constr3lem4  21595  constr3lem5  21596  vdgr1c  21637  eupares  21658  eupap1  21659  vdegp1ai  21667  vdegp1bi  21668  avril1  21718  vafval  22043  smfval  22045  0vfval  22046  nmcvfval  22047  vsfval  22075  pjoc2i  22901  pjcji  23147  ho0val  23214  hoival  23219  adjbdlnb  23548  nmopcoadji  23565  opsqrlem2  23605  opsqrlem5  23608  hmopidmchi  23615  hmopidmpji  23616  pjinvari  23655  pjadj2coi  23668  pj3lem1  23670  funcnvmptOLD  24043  funcnvmpt  24044  cnre2csqlem  24269  zzsnm  24303  rrhcn  24341  qqhre  24347  coinflippv  24702  eflgam  24790  derangenlem  24818  kur14lem2  24854  kur14lem3  24855  kur14lem5  24857  kur14lem6  24858  txsconlem  24888  cvmliftlem4  24936  cvmliftlem5  24937  cbvprod  25202  fprodss  25235  fprodefsum  25259  iprodclim3  25274  trpredmintr  25456  trpred0  25461  wfrlem5  25482  frrlem5  25507  funpartfv  25706  fullfunfv  25708  axlowdimlem8  25800  axlowdimlem9  25801  axlowdimlem11  25803  axlowdimlem12  25804  axlowdimlem17  25809  ftc1cnnc  26186  neibastop2lem  26287  heiborlem4  26421  heiborlem6  26423  rabdiophlem2  26760  dnnumch1  27017  aomclem6  27032  mncn0  27220  aaitgo  27243  rngunsnply  27254  symggen  27287  cytpval  27404  fmul01  27585  fmuldfeq  27588  fmul01lt1lem1  27589  fmul01lt1lem2  27590  itgsin0pilem1  27619  stoweidlem3  27627  stoweidlem17  27641  stoweidlem47  27671  cdlemk13  31346  cdlemk14  31348  cdlemk15  31349  cdlemk21N  31367  cdlemk20  31368  cdlemk56w  31467  lcfrlem1  32037  hdmapfval  32325
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2393
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2399  df-cleq 2405  df-clel 2408  df-nfc 2537  df-rex 2680  df-uni 3984  df-br 4181  df-iota 5385  df-fv 5429
  Copyright terms: Public domain W3C validator