Theorem fveq1d 5672

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 5669	. 2 ⊢ (𝐹 = 𝐺 → (𝐹‘𝐴) = (𝐺‘𝐴))
3	1, 2	syl 14	1 ⊢ (𝜑 → (𝐹‘𝐴) = (𝐺‘𝐴))

Syntax hints:   → wi 4   = wceq 1398  ‘cfv 5352

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2214

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-rex 2526  df-uni 3915  df-br 4110  df-iota 5312  df-fv 5360

This theorem is referenced by:  fveq12d  5677  funssfv  5696  fv2prc  5709  csbfv2g  5711  fvco4  5749  fvmptd  5758  fvmpt2d  5764  mpteqb  5768  fvmptt  5769  fnmptfvd  5782  fmptco  5843  fvunsng  5878  fvsng  5880  fsnunfv  5885  f1ocnvfv1  5950  f1ocnvfv2  5951  fcof1  5956  fcofo  5957  ofvalg  6276  offval2  6282  ofrfval2  6283  caofinvl  6292  tfrlemi1  6563  rdg0g  6619  freceq1  6623  oav  6687  omv  6688  oeiv  6689  pw2f1odclem  7087  mapxpen  7101  xpmapenlem  7102  2omap  7269  nninfisollemne  7422  nninfisol  7424  exmidomni  7433  nninfwlpoimlemginf  7467  cc3  7582  fseq1p1m1  10428  seqeq3  10814  seq3f1olemqsum  10875  seq3f1olemstep  10876  seq3f1olemp  10877  seqf1oglem2  10882  seqf1og  10883  seq3id  10887  seq3z  10890  exp3val  10903  bcval5  11125  bcn2  11126  seq3coll  11214  s1fv  11314  ccat1st1st  11329  ccat2s1fvwd  11335  swrdfv  11345  pfxfv  11376  swrdswrd  11397  shftcan1  11519  shftcan2  11520  shftvalg  11521  shftval4g  11522  climshft2  11991  sumeq2  12044  summodc  12069  zsumdc  12070  fsum3  12073  isumz  12075  fisumss  12078  fsum3cvg2  12080  isumsplit  12177  prodeq2w  12242  prodeq2  12243  prodmodc  12264  zproddc  12265  fprodseq  12269  prod1dc  12272  fprodssdc  12276  nninfctlemfo  12736  odzval  12939  1arithlem2  13062  fvsetsid  13246  setsslid  13263  setsslnid  13264  prdsex  13482  prdsval  13486  prdsplusgfval  13497  prdsmulrfval  13499  imasival  13519  imasbas  13520  imasplusg  13521  imasmulr  13522  igsumvalx  13602  gsumfzval  13604  gsumpropd  13605  gsumress  13608  gsumval2  13610  grpinvval  13756  grpsubfvalg  13758  grpsubpropdg  13817  grpsubpropd2  13818  pwsinvg  13825  mulgfvalg  13838  mulgpropdg  13881  submmulg  13883  subgmulg  13905  releqgg  13937  eqgex  13938  eqgfval  13939  gsumfzmptfidmadd  14056  unitinvcl  14268  unitinvinv  14269  unitlinv  14271  unitrinv  14272  unitnegcl  14275  dvrfvald  14278  dvrvald  14279  rdivmuldivd  14289  subrgugrp  14385  rrgsupp  14411  lspval  14538  ixpsnbasval  14614  lidlnegcl  14633  rspcl  14639  rspssid  14640  rspssp  14642  rspsn  14682  zrhmulg  14768  znzrhval  14795  mplsubgfilemm  14853  mplsubgfilemcl  14854  mplsubgfileminv  14855  mplnegfi  14860  ntrval  14975  clsval  14976  neival  15008  cnpval  15063  txmetcnp  15383  metcnpd  15385  limccl  15524  ellimc3apf  15525  cnplimclemr  15534  limccnp2cntop  15542  dvfvalap  15546  dvfre  15575  plycoeid3  15622  plyrecj  15628  lgsval4  15893  lgsmod  15899  uhgrspansubgrlem  16271  vtxdgfval  16283  vtxdgfifival  16286  vtxdgop  16287  vtxdeqd  16291  vtxdfifiun  16292  1loopgrvd0fi  16301  1hevtxdg0fi  16302  1hevtxdg1en  16303  1hegrvtxdg1fi  16304  wksfval  16317  wlkres  16374  eupth2fi  16474  pw1map  16769  peano4nninf  16784  gsumgfsumlem  16865