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

Theorem fveq1i 5669
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 5667 . 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 5394
This theorem is referenced by:  fveq12i  5673  fvun2  5734  fvopab3ig  5742  fvsnun1  5867  fvsnun2  5868  fvpr1  5874  fvpr2  5875  fvpr1g  5876  fvpr2g  5877  fvtp1  5878  fvtp2  5879  fvtp3  5880  fvtp1g  5881  fvtp2g  5882  fvtp3g  5883  fvresex  5921  fveqf1o  5968  ov  6132  ovigg  6133  ovg  6151  curry1  6377  curry2  6380  tfr2a  6592  rdgsucmptf  6622  rdgsucmptnf  6623  frsucmpt  6631  frsucmptn  6632  seqomlem1  6643  seqomlem3  6645  seqomlem4  6646  seqom0g  6649  seqomsuc  6650  abianfplem  6651  unblem2  7296  inf3lemb  7513  inf3lemc  7514  trcl  7597  r10  7627  r1sucg  7628  r1limg  7630  infxpenc2  7836  aleph0  7880  alephlim  7881  alephsuc  7882  alephfplem1  7918  alephfplem2  7919  ackbij2lem3  8054  cfsmolem  8083  infpssrlem1  8116  infpssrlem2  8117  fin23lem34  8159  fin23lem35  8160  isf32lem6  8171  isf32lem7  8172  isf32lem8  8173  isf34lem5  8191  hsmexlem7  8236  axdclem2  8333  canthp1lem2  8461  wunex2  8546  wuncval2  8555  addpiord  8694  mulpiord  8695  addpqnq  8748  mulpqnq  8751  fseq1p1m1  11052  om2uz0i  11214  om2uzrdg  11223  uzrdg0i  11226  uzrdgsuci  11227  hashkf  11547  hashgval  11548  hashinf  11550  revs1  11724  cats1fv  11750  shftidt  11824  fsumss  12446  isumclim3  12470  isumsup2  12553  ruclem4  12760  ruclem6  12761  ruclem7  12762  sadc0  12893  sadcp1  12894  sadcaddlem  12896  sadaddlem  12905  smup0  12918  smupp1  12919  algr0  12990  algrp1  12992  ndxarg  13416  strfv2d  13426  xpsc0  13712  xpsc1  13713  funcoppc  13999  fthepi  14052  homadm  14122  homacd  14123  prdsidlem  14654  prdsinvlem  14853  cayleylem2  15038  gsumval3  15441  gsumzaddlem  15453  gsumzmhm  15460  pgpfaclem1  15566  rngidval  15593  lidlval  16192  rspval  16193  lidlnegcl  16212  lpival  16243  znf1o  16755  restcls  17167  restntr  17168  upxp  17576  cnmetdval  18676  remetdval  18691  qdensere2  18699  pcoptcl  18917  pcopt  18918  pcopt2  18919  pcorevlem  18922  ovolfsval  19234  ovollb2lem  19251  ovolunlem1a  19259  ovoliunlem1  19265  ovoliun2  19269  ovolscalem1  19276  ovolicc2lem4  19283  mblvol  19293  ioombl1lem4  19322  uniioovol  19338  uniioombllem3  19344  0pval  19430  limccnp  19645  limccnp2  19646  dvcnvrelem2  19769  itgsubstlem  19799  evl1val  19815  ply1remlem  19952  plyrem  20089  qaa  20107  abelth  20224  efif1olem4  20314  eflog  20341  logef  20343  logeftb  20345  dvrelog  20395  dvlog  20409  cxpcn3  20499  efrlim  20675  wilthlem3  20720  basellem8  20737  lgsqrlem1  20992  wlkntrllem4  21416  wlkntrllem5  21417  constr3lem4  21482  constr3lem5  21483  vdgr1c  21524  eupares  21545  eupap1  21546  vdegp1ai  21554  vdegp1bi  21555  avril1  21605  vafval  21930  smfval  21932  0vfval  21933  nmcvfval  21934  vsfval  21962  pjoc2i  22788  pjcji  23034  ho0val  23101  hoival  23106  adjbdlnb  23435  nmopcoadji  23452  opsqrlem2  23492  opsqrlem5  23495  hmopidmchi  23502  hmopidmpji  23503  pjinvari  23542  pjadj2coi  23555  pj3lem1  23557  funcnvmptOLD  23923  funcnvmpt  23924  cnre2csqlem  24112  zzsnm  24144  rrhcn  24179  qqhre  24182  coinflippv  24520  eflgam  24608  derangenlem  24636  kur14lem2  24672  kur14lem3  24673  kur14lem5  24675  kur14lem6  24676  txsconlem  24706  cvmliftlem4  24754  cvmliftlem5  24755  cbvprod  25020  fprodss  25053  fprodefsum  25077  iprodclim3  25085  trpredmintr  25258  trpred0  25263  wfrlem5  25284  frrlem5  25309  funpartfv  25508  fullfunfv  25510  axlowdimlem8  25602  axlowdimlem9  25603  axlowdimlem11  25605  axlowdimlem12  25606  axlowdimlem17  25611  ftc1cnnc  25979  neibastop2lem  26080  heiborlem4  26214  heiborlem6  26216  rabdiophlem2  26553  dnnumch1  26810  aomclem6  26825  mncn0  27013  aaitgo  27036  rngunsnply  27047  symggen  27080  cytpval  27197  fmul01  27378  fmuldfeq  27381  fmul01lt1lem1  27382  fmul01lt1lem2  27383  itgsin0pilem1  27412  stoweidlem3  27420  stoweidlem17  27434  stoweidlem47  27464  cdlemk13  30966  cdlemk14  30968  cdlemk15  30969  cdlemk21N  30987  cdlemk20  30988  cdlemk56w  31087  lcfrlem1  31657  hdmapfval  31945
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 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2368
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2374  df-cleq 2380  df-clel 2383  df-nfc 2512  df-rex 2655  df-uni 3958  df-br 4154  df-iota 5358  df-fv 5402
  Copyright terms: Public domain W3C validator