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

Theorem fveq1i 5688
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 5686 . 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 5413
This theorem is referenced by:  fveq12i  5692  fvun2  5754  fvopab3ig  5762  fvsnun1  5887  fvsnun2  5888  fvpr1  5894  fvpr2  5895  fvpr1g  5896  fvpr2g  5897  fvtp1  5898  fvtp2  5899  fvtp3  5900  fvtp1g  5901  fvtp2g  5902  fvtp3g  5903  fvresex  5941  fveqf1o  5988  ov  6152  ovigg  6153  ovg  6171  curry1  6397  curry2  6400  tfr2a  6615  rdgsucmptf  6645  rdgsucmptnf  6646  frsucmpt  6654  frsucmptn  6655  seqomlem1  6666  seqomlem3  6668  seqomlem4  6669  seqom0g  6672  seqomsuc  6673  abianfplem  6674  unblem2  7319  inf3lemb  7536  inf3lemc  7537  trcl  7620  r10  7650  r1sucg  7651  r1limg  7653  infxpenc2  7859  aleph0  7903  alephlim  7904  alephsuc  7905  alephfplem1  7941  alephfplem2  7942  ackbij2lem3  8077  cfsmolem  8106  infpssrlem1  8139  infpssrlem2  8140  fin23lem34  8182  fin23lem35  8183  isf32lem6  8194  isf32lem7  8195  isf32lem8  8196  isf34lem5  8214  hsmexlem7  8259  axdclem2  8356  canthp1lem2  8484  wunex2  8569  wuncval2  8578  addpiord  8717  mulpiord  8718  addpqnq  8771  mulpqnq  8774  fseq1p1m1  11077  om2uz0i  11242  om2uzrdg  11251  uzrdg0i  11254  uzrdgsuci  11255  hashkf  11575  hashgval  11576  hashinf  11578  revs1  11752  cats1fv  11778  shftidt  11852  fsumss  12474  isumclim3  12498  isumsup2  12581  ruclem4  12788  ruclem6  12789  ruclem7  12790  sadc0  12921  sadcp1  12922  sadcaddlem  12924  sadaddlem  12933  smup0  12946  smupp1  12947  algr0  13018  algrp1  13020  ndxarg  13444  strfv2d  13454  xpsc0  13740  xpsc1  13741  funcoppc  14027  fthepi  14080  homadm  14150  homacd  14151  prdsidlem  14682  prdsinvlem  14881  cayleylem2  15066  gsumval3  15469  gsumzaddlem  15481  gsumzmhm  15488  pgpfaclem1  15594  rngidval  15621  lidlval  16220  rspval  16221  lidlnegcl  16240  lpival  16271  znf1o  16787  restcls  17199  restntr  17200  upxp  17608  cnmetdval  18758  remetdval  18773  qdensere2  18781  pcoptcl  18999  pcopt  19000  pcopt2  19001  pcorevlem  19004  ovolfsval  19320  ovollb2lem  19337  ovolunlem1a  19345  ovoliunlem1  19351  ovoliun2  19355  ovolscalem1  19362  ovolicc2lem4  19369  mblvol  19379  ioombl1lem4  19408  uniioovol  19424  uniioombllem3  19430  0pval  19516  limccnp  19731  limccnp2  19732  dvcnvrelem2  19855  itgsubstlem  19885  evl1val  19901  ply1remlem  20038  plyrem  20175  qaa  20193  abelth  20310  efif1olem4  20400  eflog  20427  logef  20429  logeftb  20431  dvrelog  20481  dvlog  20495  cxpcn3  20585  efrlim  20761  wilthlem3  20806  basellem8  20823  lgsqrlem1  21078  2wlklemA  21507  2wlklemB  21508  2wlklemC  21509  wlkntrllem2  21513  wlkntrllem3  21514  constr3lem4  21587  constr3lem5  21588  vdgr1c  21629  eupares  21650  eupap1  21651  vdegp1ai  21659  vdegp1bi  21660  avril1  21710  vafval  22035  smfval  22037  0vfval  22038  nmcvfval  22039  vsfval  22067  pjoc2i  22893  pjcji  23139  ho0val  23206  hoival  23211  adjbdlnb  23540  nmopcoadji  23557  opsqrlem2  23597  opsqrlem5  23600  hmopidmchi  23607  hmopidmpji  23608  pjinvari  23647  pjadj2coi  23660  pj3lem1  23662  funcnvmptOLD  24035  funcnvmpt  24036  cnre2csqlem  24261  zzsnm  24295  rrhcn  24333  qqhre  24339  coinflippv  24694  eflgam  24782  derangenlem  24810  kur14lem2  24846  kur14lem3  24847  kur14lem5  24849  kur14lem6  24850  txsconlem  24880  cvmliftlem4  24928  cvmliftlem5  24929  cbvprod  25194  fprodss  25227  fprodefsum  25251  iprodclim3  25266  trpredmintr  25448  trpred0  25453  wfrlem5  25474  frrlem5  25499  funpartfv  25698  fullfunfv  25700  axlowdimlem8  25792  axlowdimlem9  25793  axlowdimlem11  25795  axlowdimlem12  25796  axlowdimlem17  25801  ftc1cnnc  26178  neibastop2lem  26279  heiborlem4  26413  heiborlem6  26415  rabdiophlem2  26752  dnnumch1  27009  aomclem6  27024  mncn0  27212  aaitgo  27235  rngunsnply  27246  symggen  27279  cytpval  27396  fmul01  27577  fmuldfeq  27580  fmul01lt1lem1  27581  fmul01lt1lem2  27582  itgsin0pilem1  27611  stoweidlem3  27619  stoweidlem17  27633  stoweidlem47  27663  cdlemk13  31334  cdlemk14  31336  cdlemk15  31337  cdlemk21N  31355  cdlemk20  31356  cdlemk56w  31455  lcfrlem1  32025  hdmapfval  32313
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 2385
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 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-rex 2672  df-uni 3976  df-br 4173  df-iota 5377  df-fv 5421
  Copyright terms: Public domain W3C validator