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

Theorem fveq1i 5730
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 5728 . 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 1653   ` cfv 5455
This theorem is referenced by:  fveq12i  5734  fvun2  5796  fvopab3ig  5804  fvsnun1  5929  fvsnun2  5930  fvpr1  5936  fvpr2  5937  fvpr1g  5938  fvpr2g  5939  fvtp1  5940  fvtp2  5941  fvtp3  5942  fvtp1g  5943  fvtp2g  5944  fvtp3g  5945  fvresex  5983  fveqf1o  6030  ov  6194  ovigg  6195  ovg  6213  curry1  6439  curry2  6442  tfr2a  6657  rdgsucmptf  6687  rdgsucmptnf  6688  frsucmpt  6696  frsucmptn  6697  seqomlem1  6708  seqomlem3  6710  seqomlem4  6711  seqom0g  6714  seqomsuc  6715  abianfplem  6716  unblem2  7361  inf3lemb  7581  inf3lemc  7582  trcl  7665  r10  7695  r1sucg  7696  r1limg  7698  infxpenc2  7904  aleph0  7948  alephlim  7949  alephsuc  7950  alephfplem1  7986  alephfplem2  7987  ackbij2lem3  8122  cfsmolem  8151  infpssrlem1  8184  infpssrlem2  8185  fin23lem34  8227  fin23lem35  8228  isf32lem6  8239  isf32lem7  8240  isf32lem8  8241  isf34lem5  8259  hsmexlem7  8304  axdclem2  8401  canthp1lem2  8529  wunex2  8614  wuncval2  8623  addpiord  8762  mulpiord  8763  addpqnq  8816  mulpqnq  8819  fseq1p1m1  11123  om2uz0i  11288  om2uzrdg  11297  uzrdg0i  11300  uzrdgsuci  11301  hashkf  11621  hashgval  11622  hashinf  11624  revs1  11798  cats1fv  11824  shftidt  11898  fsumss  12520  isumclim3  12544  isumsup2  12627  ruclem4  12834  ruclem6  12835  ruclem7  12836  sadc0  12967  sadcp1  12968  sadcaddlem  12970  sadaddlem  12979  smup0  12992  smupp1  12993  algr0  13064  algrp1  13066  ndxarg  13490  strfv2d  13500  xpsc0  13786  xpsc1  13787  funcoppc  14073  fthepi  14126  homadm  14196  homacd  14197  prdsidlem  14728  prdsinvlem  14927  cayleylem2  15112  gsumval3  15515  gsumzaddlem  15527  gsumzmhm  15534  pgpfaclem1  15640  rngidval  15667  lidlval  16266  rspval  16267  lidlnegcl  16286  lpival  16317  znf1o  16833  restcls  17246  restntr  17247  upxp  17656  cnmetdval  18806  remetdval  18821  qdensere2  18829  pcoptcl  19047  pcopt  19048  pcopt2  19049  pcorevlem  19052  ovolfsval  19368  ovollb2lem  19385  ovolunlem1a  19393  ovoliunlem1  19399  ovoliun2  19403  ovolscalem1  19410  ovolicc2lem4  19417  mblvol  19427  ioombl1lem4  19456  uniioovol  19472  uniioombllem3  19478  0pval  19564  limccnp  19779  limccnp2  19780  dvcnvrelem2  19903  itgsubstlem  19933  evl1val  19949  ply1remlem  20086  plyrem  20223  qaa  20241  abelth  20358  efif1olem4  20448  eflog  20475  logef  20477  logeftb  20479  dvrelog  20529  dvlog  20543  cxpcn3  20633  efrlim  20809  wilthlem3  20854  basellem8  20871  lgsqrlem1  21126  2wlklemA  21555  2wlklemB  21556  2wlklemC  21557  wlkntrllem2  21561  wlkntrllem3  21562  constr3lem4  21635  constr3lem5  21636  vdgr1c  21677  eupares  21698  eupap1  21699  vdegp1ai  21707  vdegp1bi  21708  avril1  21758  vafval  22083  smfval  22085  0vfval  22086  nmcvfval  22087  vsfval  22115  pjoc2i  22941  pjcji  23187  ho0val  23254  hoival  23259  adjbdlnb  23588  nmopcoadji  23605  opsqrlem2  23645  opsqrlem5  23648  hmopidmchi  23655  hmopidmpji  23656  pjinvari  23695  pjadj2coi  23708  pj3lem1  23710  funcnvmptOLD  24083  funcnvmpt  24084  cnre2csqlem  24309  zzsnm  24343  rrhcn  24381  qqhre  24387  coinflippv  24742  eflgam  24830  derangenlem  24858  kur14lem2  24894  kur14lem3  24895  kur14lem5  24897  kur14lem6  24898  txsconlem  24928  cvmliftlem4  24976  cvmliftlem5  24977  cbvprod  25242  fprodss  25275  fprodefsum  25299  iprodclim3  25314  trpredmintr  25510  trpred0  25515  wfrlem5  25543  frrlem5  25587  funpartfv  25791  fullfunfv  25793  axlowdimlem8  25889  axlowdimlem9  25890  axlowdimlem11  25892  axlowdimlem12  25893  axlowdimlem17  25898  ftc1cnnc  26280  neibastop2lem  26390  heiborlem4  26524  heiborlem6  26526  rabdiophlem2  26863  dnnumch1  27120  aomclem6  27135  mncn0  27322  aaitgo  27345  rngunsnply  27356  symggen  27389  cytpval  27506  fmul01  27687  fmuldfeq  27690  fmul01lt1lem1  27691  fmul01lt1lem2  27692  itgsin0pilem1  27721  stoweidlem3  27729  stoweidlem17  27743  stoweidlem47  27773  cdlemk13  31650  cdlemk14  31652  cdlemk15  31653  cdlemk21N  31671  cdlemk20  31672  cdlemk56w  31771  lcfrlem1  32341  hdmapfval  32629
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2418
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2424  df-cleq 2430  df-clel 2433  df-nfc 2562  df-rex 2712  df-uni 4017  df-br 4214  df-iota 5419  df-fv 5463
  Copyright terms: Public domain W3C validator