Theorem fveq1d 5641

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

Syntax hints:   → wi 4   = wceq 1397  ‘cfv 5326

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-rex 2516  df-uni 3894  df-br 4089  df-iota 5286  df-fv 5334

This theorem is referenced by:  fveq12d  5646  funssfv  5665  fv2prc  5678  csbfv2g  5680  fvco4  5718  fvmptd  5727  fvmpt2d  5733  mpteqb  5737  fvmptt  5738  fnmptfvd  5751  fmptco  5813  fvunsng  5847  fvsng  5849  fsnunfv  5854  f1ocnvfv1  5917  f1ocnvfv2  5918  fcof1  5923  fcofo  5924  ofvalg  6244  offval2  6250  ofrfval2  6251  caofinvl  6260  tfrlemi1  6497  rdg0g  6553  freceq1  6557  oav  6621  omv  6622  oeiv  6623  pw2f1odclem  7019  mapxpen  7033  xpmapenlem  7034  nninfisollemne  7329  nninfisol  7331  exmidomni  7340  nninfwlpoimlemginf  7374  cc3  7486  fseq1p1m1  10328  seqeq3  10713  seq3f1olemqsum  10774  seq3f1olemstep  10775  seq3f1olemp  10776  seqf1oglem2  10781  seqf1og  10782  seq3id  10786  seq3z  10789  exp3val  10802  bcval5  11024  bcn2  11025  seq3coll  11105  s1fv  11202  ccat1st1st  11217  ccat2s1fvwd  11223  swrdfv  11233  pfxfv  11264  swrdswrd  11285  shftcan1  11394  shftcan2  11395  shftvalg  11396  shftval4g  11397  climshft2  11866  sumeq2  11919  summodc  11943  zsumdc  11944  fsum3  11947  isumz  11949  fisumss  11952  fsum3cvg2  11954  isumsplit  12051  prodeq2w  12116  prodeq2  12117  prodmodc  12138  zproddc  12139  fprodseq  12143  prod1dc  12146  fprodssdc  12150  nninfctlemfo  12610  odzval  12813  1arithlem2  12936  fvsetsid  13115  setsslid  13132  setsslnid  13133  prdsex  13351  prdsval  13355  prdsplusgfval  13366  prdsmulrfval  13368  imasival  13388  imasbas  13389  imasplusg  13390  imasmulr  13391  igsumvalx  13471  gsumfzval  13473  gsumpropd  13474  gsumress  13477  gsumval2  13479  grpinvval  13625  grpsubfvalg  13627  grpsubpropdg  13686  grpsubpropd2  13687  pwsinvg  13694  mulgfvalg  13707  mulgpropdg  13750  submmulg  13752  subgmulg  13774  releqgg  13806  eqgex  13807  eqgfval  13808  gsumfzmptfidmadd  13925  unitinvcl  14136  unitinvinv  14137  unitlinv  14139  unitrinv  14140  unitnegcl  14143  dvrfvald  14146  dvrvald  14147  rdivmuldivd  14157  subrgugrp  14253  lspval  14403  ixpsnbasval  14479  lidlnegcl  14498  rspcl  14504  rspssid  14505  rspssp  14507  rspsn  14547  zrhmulg  14633  znzrhval  14660  mplsubgfilemm  14711  mplsubgfilemcl  14712  mplsubgfileminv  14713  mplnegfi  14718  ntrval  14833  clsval  14834  neival  14866  cnpval  14921  txmetcnp  15241  metcnpd  15243  limccl  15382  ellimc3apf  15383  cnplimclemr  15392  limccnp2cntop  15400  dvfvalap  15404  dvfre  15433  plycoeid3  15480  plyrecj  15486  lgsval4  15748  lgsmod  15754  uhgrspansubgrlem  16126  vtxdgfval  16138  vtxdgfifival  16141  vtxdgop  16142  vtxdeqd  16146  vtxdfifiun  16147  1loopgrvd0fi  16156  1hevtxdg0fi  16157  1hevtxdg1en  16158  1hegrvtxdg1fi  16159  wksfval  16172  wlkres  16229  2omap  16594  pw1map  16596  peano4nninf  16608  gsumgfsumlem  16683