Theorem fveq1d 5637

Description: Equality deduction for function value. (Contributed by NM, 2-Sep-2003.)

Hypothesis

Ref	Expression
fveq1d.1	⊢ (𝜑 → 𝐹 = 𝐺)

Assertion

Ref	Expression
fveq1d	⊢ (𝜑 → (𝐹‘𝐴) = (𝐺‘𝐴))

Proof of Theorem fveq1d

Step	Hyp	Ref	Expression
1		fveq1d.1	. 2 ⊢ (𝜑 → 𝐹 = 𝐺)
2		fveq1 5634	. 2 ⊢ (𝐹 = 𝐺 → (𝐹‘𝐴) = (𝐺‘𝐴))
3	1, 2	syl 14	1 ⊢ (𝜑 → (𝐹‘𝐴) = (𝐺‘𝐴))

Syntax hints:   → wi 4   = wceq 1395  ‘cfv 5324

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-rex 2514  df-uni 3892  df-br 4087  df-iota 5284  df-fv 5332

This theorem is referenced by:  fveq12d  5642  funssfv  5661  fv2prc  5674  csbfv2g  5676  fvco4  5714  fvmptd  5723  fvmpt2d  5729  mpteqb  5733  fvmptt  5734  fnmptfvd  5747  fmptco  5809  fvunsng  5843  fvsng  5845  fsnunfv  5850  f1ocnvfv1  5913  f1ocnvfv2  5914  fcof1  5919  fcofo  5920  ofvalg  6240  offval2  6246  ofrfval2  6247  caofinvl  6256  tfrlemi1  6493  rdg0g  6549  freceq1  6553  oav  6617  omv  6618  oeiv  6619  pw2f1odclem  7015  mapxpen  7029  xpmapenlem  7030  nninfisollemne  7321  nninfisol  7323  exmidomni  7332  nninfwlpoimlemginf  7366  cc3  7477  fseq1p1m1  10319  seqeq3  10704  seq3f1olemqsum  10765  seq3f1olemstep  10766  seq3f1olemp  10767  seqf1oglem2  10772  seqf1og  10773  seq3id  10777  seq3z  10780  exp3val  10793  bcval5  11015  bcn2  11016  seq3coll  11096  s1fv  11193  ccat1st1st  11208  ccat2s1fvwd  11214  swrdfv  11224  pfxfv  11255  swrdswrd  11276  shftcan1  11385  shftcan2  11386  shftvalg  11387  shftval4g  11388  climshft2  11857  sumeq2  11910  summodc  11934  zsumdc  11935  fsum3  11938  isumz  11940  fisumss  11943  fsum3cvg2  11945  isumsplit  12042  prodeq2w  12107  prodeq2  12108  prodmodc  12129  zproddc  12130  fprodseq  12134  prod1dc  12137  fprodssdc  12141  nninfctlemfo  12601  odzval  12804  1arithlem2  12927  fvsetsid  13106  setsslid  13123  setsslnid  13124  prdsex  13342  prdsval  13346  prdsplusgfval  13357  prdsmulrfval  13359  imasival  13379  imasbas  13380  imasplusg  13381  imasmulr  13382  igsumvalx  13462  gsumfzval  13464  gsumpropd  13465  gsumress  13468  gsumval2  13470  grpinvval  13616  grpsubfvalg  13618  grpsubpropdg  13677  grpsubpropd2  13678  pwsinvg  13685  mulgfvalg  13698  mulgpropdg  13741  submmulg  13743  subgmulg  13765  releqgg  13797  eqgex  13798  eqgfval  13799  gsumfzmptfidmadd  13916  unitinvcl  14127  unitinvinv  14128  unitlinv  14130  unitrinv  14131  unitnegcl  14134  dvrfvald  14137  dvrvald  14138  rdivmuldivd  14148  subrgugrp  14244  lspval  14394  ixpsnbasval  14470  lidlnegcl  14489  rspcl  14495  rspssid  14496  rspssp  14498  rspsn  14538  zrhmulg  14624  znzrhval  14651  mplsubgfilemm  14702  mplsubgfilemcl  14703  mplsubgfileminv  14704  mplnegfi  14709  ntrval  14824  clsval  14825  neival  14857  cnpval  14912  txmetcnp  15232  metcnpd  15234  limccl  15373  ellimc3apf  15374  cnplimclemr  15383  limccnp2cntop  15391  dvfvalap  15395  dvfre  15424  plycoeid3  15471  plyrecj  15477  lgsval4  15739  lgsmod  15745  vtxdgfval  16094  vtxdgfifival  16097  vtxdgop  16098  vtxdeqd  16102  vtxdfifiun  16103  1loopgrvd0fi  16112  1hevtxdg0fi  16113  wksfval  16119  wlkres  16174  2omap  16530  pw1map  16532  peano4nninf  16544