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

Theorem fveq1i 5680
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 5678 . 2  |-  ( F  =  G  ->  ( F `  A )  =  ( G `  A ) )
31, 2ax-mp 5 1  |-  ( F `
 A )  =  ( G `  A
)
Colors of variables: wff setvar class
Syntax hints:    = wceq 1362   ` cfv 5406
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-rex 2711  df-uni 4080  df-br 4281  df-iota 5369  df-fv 5414
This theorem is referenced by:  fveq12i  5684  fvun2  5751  fvopab3ig  5759  fvsnun1  5900  fvsnun2  5901  fvpr1  5908  fvpr2  5909  fvpr1g  5910  fvpr2g  5911  fvtp1  5912  fvtp2  5913  fvtp3  5914  fvtp1g  5915  fvtp2g  5916  fvtp3g  5917  fveqf1o  5987  ov  6199  ovigg  6200  ovg  6218  fvresex  6539  curry1  6653  curry2  6656  suppsnop  6693  tfr2a  6840  rdgsucmptf  6870  rdgsucmptnf  6871  frsucmpt  6879  frsucmptn  6880  seqomlem1  6891  seqomlem3  6893  seqomlem4  6894  seqom0g  6897  seqomsuc  6898  abianfplem  6899  unblem2  7553  inf3lemb  7819  inf3lemc  7820  trcl  7936  r10  7963  r1sucg  7964  r1limg  7966  infxpenc2  8176  infxpenc2OLD  8180  aleph0  8224  alephlim  8225  alephsuc  8226  alephfplem1  8262  alephfplem2  8263  ackbij2lem3  8398  cfsmolem  8427  infpssrlem1  8460  infpssrlem2  8461  fin23lem34  8503  fin23lem35  8504  isf32lem6  8515  isf32lem7  8516  isf32lem8  8517  isf34lem5  8535  hsmexlem7  8580  axdclem2  8677  canthp1lem2  8807  wunex2  8892  wuncval2  8901  addpiord  9040  mulpiord  9041  addpqnq  9094  mulpqnq  9097  fseq1p1m1  11517  om2uz0i  11753  om2uzrdg  11762  uzrdg0i  11765  uzrdgsuci  11766  hashkf  12088  hashgval  12089  hashinf  12091  revs1  12388  cats1fv  12469  shftidt  12554  cbvsum  13155  fsumss  13185  isumclim3  13209  isumsup2  13291  ruclem4  13498  ruclem6  13499  ruclem7  13500  sadc0  13632  sadcp1  13633  sadcaddlem  13635  sadaddlem  13644  smup0  13657  smupp1  13658  algr0  13729  algrp1  13731  ndxarg  14176  strfv2d  14188  xpsc0  14480  xpsc1  14481  funcoppc  14767  fthepi  14820  homadm  14890  homacd  14891  prdsidlem  15435  prdsinvlem  15642  cayleylem2  15897  symggen  15955  pmtr3ncomlem1  15958  gsumval3OLD  16361  gsumval3  16364  gsumzaddlem  16387  gsumzaddlemOLD  16389  gsumzmhm  16406  gsumzmhmOLD  16407  pgpfaclem1  16555  rngidval  16582  lidlval  17194  rspval  17195  lidlnegcl  17217  lpival  17248  znf1o  17825  mdetralt  18255  mdetunilem7  18265  restcls  18626  restntr  18627  upxp  19037  cnmetdval  20191  remetdval  20207  qdensere2  20215  pcoptcl  20434  pcopt  20435  pcopt2  20436  pcorevlem  20439  ovolfsval  20795  ovollb2lem  20812  ovolunlem1a  20820  ovoliunlem1  20826  ovoliun2  20830  ovolscalem1  20837  ovolicc2lem4  20844  mblvol  20854  ioombl1lem4  20883  uniioovol  20900  uniioombllem3  20906  0pval  20990  limccnp  21207  limccnp2  21208  dvcnvrelem2  21331  itgsubstlem  21361  evl1val  21378  ply1remlem  21518  plyrem  21655  qaa  21673  abelth  21790  efif1olem4  21885  eflog  21912  logef  21914  logeftb  21916  dvrelog  21966  dvlog  21980  cxpcn3  22070  efrlim  22247  wilthlem3  22292  basellem8  22309  lgsqrlem1  22564  axlowdimlem8  23017  axlowdimlem9  23018  axlowdimlem11  23020  axlowdimlem12  23021  axlowdimlem17  23026  2wlklemA  23275  2wlklemB  23276  2wlklemC  23277  wlkntrllem2  23281  wlkntrllem3  23282  constr3lem4  23355  constr3lem5  23356  vdgr1c  23397  eupares  23418  eupap1  23419  vdegp1ai  23427  vdegp1bi  23428  avril1  23478  vafval  23803  smfval  23805  0vfval  23806  nmcvfval  23807  vsfval  23835  pjoc2i  24663  pjcji  24909  ho0val  24976  hoival  24981  adjbdlnb  25310  nmopcoadji  25327  opsqrlem2  25367  opsqrlem5  25370  hmopidmchi  25377  hmopidmpji  25378  pjinvari  25417  pjadj2coi  25430  pj3lem1  25432  funcnvmptOLD  25809  funcnvmpt  25810  cnre2csqlem  26193  zzsnm  26242  zzsnmOLD  26243  rrhcn  26279  qqhre  26299  eulerpart  26612  fib0  26629  fib1  26630  fibp1  26631  coinflippv  26713  gsumnunsn  26784  eflgam  26878  derangenlem  26906  kur14lem2  26942  kur14lem3  26943  kur14lem5  26945  kur14lem6  26946  txsconlem  26976  cvmliftlem4  27024  cvmliftlem5  27025  cbvprod  27274  fprodss  27307  fprodefsum  27331  iprodclim3  27346  trpredmintr  27541  trpred0  27546  wfrlem5  27574  frrlem5  27618  funpartfv  27822  fullfunfv  27824  ftc1cnnc  28307  neibastop2lem  28422  heiborlem4  28554  heiborlem6  28556  rabdiophlem2  28982  dnnumch1  29239  aomclem6  29254  mncn0  29338  aaitgo  29361  rngunsnply  29372  cytpval  29419  fmul01  29603  fmuldfeq  29606  fmul01lt1lem1  29607  fmul01lt1lem2  29608  itgsin0pilem1  29633  stoweidlem3  29641  stoweidlem17  29655  stoweidlem47  29685  wlkiswwlksur  30194  lineval  30633  lincvalpr  30658  lindslinindimp2lem4  30701  zlmodzxzldeplem3  30750  zlmodzxzldeplem4  30751  cdlemk13  34066  cdlemk14  34068  cdlemk15  34069  cdlemk21N  34087  cdlemk20  34088  cdlemk56w  34187  lcfrlem1  34757  hdmapfval  35045
  Copyright terms: Public domain W3C validator