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

Theorem fveq1i 5662
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 5660 . 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 5387
This theorem is referenced by:  fveq12i  5666  fvun2  5727  fvopab3ig  5735  fvsnun1  5860  fvsnun2  5861  fvpr1  5867  fvpr2  5868  fvpr1g  5869  fvpr2g  5870  fvtp1  5871  fvtp2  5872  fvtp3  5873  fvtp1g  5874  fvtp2g  5875  fvtp3g  5876  fvresex  5914  fveqf1o  5961  ov  6125  ovigg  6126  ovg  6144  curry1  6370  curry2  6373  tfr2a  6585  rdgsucmptf  6615  rdgsucmptnf  6616  frsucmpt  6624  frsucmptn  6625  seqomlem1  6636  seqomlem3  6638  seqomlem4  6639  seqom0g  6642  seqomsuc  6643  abianfplem  6644  unblem2  7289  inf3lemb  7506  inf3lemc  7507  trcl  7590  r10  7620  r1sucg  7621  r1limg  7623  infxpenc2  7829  aleph0  7873  alephlim  7874  alephsuc  7875  alephfplem1  7911  alephfplem2  7912  ackbij2lem3  8047  cfsmolem  8076  infpssrlem1  8109  infpssrlem2  8110  fin23lem34  8152  fin23lem35  8153  isf32lem6  8164  isf32lem7  8165  isf32lem8  8166  isf34lem5  8184  hsmexlem7  8229  axdclem2  8326  canthp1lem2  8454  wunex2  8539  wuncval2  8548  addpiord  8687  mulpiord  8688  addpqnq  8741  mulpqnq  8744  fseq1p1m1  11045  om2uz0i  11207  om2uzrdg  11216  uzrdg0i  11219  uzrdgsuci  11220  hashkf  11540  hashgval  11541  hashinf  11543  revs1  11717  cats1fv  11743  shftidt  11817  fsumss  12439  isumclim3  12463  isumsup2  12546  ruclem4  12753  ruclem6  12754  ruclem7  12755  sadc0  12886  sadcp1  12887  sadcaddlem  12889  sadaddlem  12898  smup0  12911  smupp1  12912  algr0  12983  algrp1  12985  ndxarg  13409  strfv2d  13419  xpsc0  13705  xpsc1  13706  funcoppc  13992  fthepi  14045  homadm  14115  homacd  14116  prdsidlem  14647  prdsinvlem  14846  cayleylem2  15031  gsumval3  15434  gsumzaddlem  15446  gsumzmhm  15453  pgpfaclem1  15559  rngidval  15586  lidlval  16185  rspval  16186  lidlnegcl  16205  lpival  16236  znf1o  16748  restcls  17160  restntr  17161  upxp  17569  cnmetdval  18669  remetdval  18684  qdensere2  18692  pcoptcl  18910  pcopt  18911  pcopt2  18912  pcorevlem  18915  ovolfsval  19227  ovollb2lem  19244  ovolunlem1a  19252  ovoliunlem1  19258  ovoliun2  19262  ovolscalem1  19269  ovolicc2lem4  19276  mblvol  19286  ioombl1lem4  19315  uniioovol  19331  uniioombllem3  19337  0pval  19423  limccnp  19638  limccnp2  19639  dvcnvrelem2  19762  itgsubstlem  19792  evl1val  19808  ply1remlem  19945  plyrem  20082  qaa  20100  abelth  20217  efif1olem4  20307  eflog  20334  logef  20336  logeftb  20338  dvrelog  20388  dvlog  20402  cxpcn3  20492  efrlim  20668  wilthlem3  20713  basellem8  20730  lgsqrlem1  20985  wlkntrllem4  21409  wlkntrllem5  21410  constr3lem4  21475  constr3lem5  21476  vdgr1c  21517  eupares  21538  eupap1  21539  vdegp1ai  21547  vdegp1bi  21548  avril1  21598  vafval  21923  smfval  21925  0vfval  21926  nmcvfval  21927  vsfval  21955  pjoc2i  22781  pjcji  23027  ho0val  23094  hoival  23099  adjbdlnb  23428  nmopcoadji  23445  opsqrlem2  23485  opsqrlem5  23488  hmopidmchi  23495  hmopidmpji  23496  pjinvari  23535  pjadj2coi  23548  pj3lem1  23550  funcnvmptOLD  23916  funcnvmpt  23917  cnre2csqlem  24105  zzsnm  24137  rrhcn  24172  qqhre  24175  coinflippv  24513  eflgam  24601  derangenlem  24629  kur14lem2  24665  kur14lem3  24666  kur14lem5  24668  kur14lem6  24669  txsconlem  24699  cvmliftlem4  24747  cvmliftlem5  24748  cbvprod  25013  fprodss  25046  fprodefsum  25070  iprodclim3  25078  trpredmintr  25251  trpred0  25256  wfrlem5  25277  frrlem5  25302  funpartfv  25501  fullfunfv  25503  axlowdimlem8  25595  axlowdimlem9  25596  axlowdimlem11  25598  axlowdimlem12  25599  axlowdimlem17  25604  ftc1cnnc  25972  neibastop2lem  26073  heiborlem4  26207  heiborlem6  26209  rabdiophlem2  26546  dnnumch1  26803  aomclem6  26818  mncn0  27006  aaitgo  27029  rngunsnply  27040  symggen  27073  cytpval  27190  fmul01  27371  fmuldfeq  27374  fmul01lt1lem1  27375  fmul01lt1lem2  27376  itgsin0pilem1  27405  stoweidlem3  27413  stoweidlem17  27427  stoweidlem47  27457  cdlemk13  31017  cdlemk14  31019  cdlemk15  31020  cdlemk21N  31038  cdlemk20  31039  cdlemk56w  31138  lcfrlem1  31708  hdmapfval  31996
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 2361
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 2367  df-cleq 2373  df-clel 2376  df-nfc 2505  df-rex 2648  df-uni 3951  df-br 4147  df-iota 5351  df-fv 5395
  Copyright terms: Public domain W3C validator