Theorem fveq1d 5634

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

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

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 3889  df-br 4084  df-iota 5281  df-fv 5329

This theorem is referenced by:  fveq12d  5639  funssfv  5658  fv2prc  5671  csbfv2g  5673  fvco4  5711  fvmptd  5720  fvmpt2d  5726  mpteqb  5730  fvmptt  5731  fnmptfvd  5744  fmptco  5806  fvunsng  5840  fvsng  5842  fsnunfv  5847  f1ocnvfv1  5910  f1ocnvfv2  5911  fcof1  5916  fcofo  5917  ofvalg  6237  offval2  6243  ofrfval2  6244  caofinvl  6253  tfrlemi1  6489  rdg0g  6545  freceq1  6549  oav  6613  omv  6614  oeiv  6615  pw2f1odclem  7008  mapxpen  7022  xpmapenlem  7023  nninfisollemne  7314  nninfisol  7316  exmidomni  7325  nninfwlpoimlemginf  7359  cc3  7470  fseq1p1m1  10307  seqeq3  10691  seq3f1olemqsum  10752  seq3f1olemstep  10753  seq3f1olemp  10754  seqf1oglem2  10759  seqf1og  10760  seq3id  10764  seq3z  10767  exp3val  10780  bcval5  11002  bcn2  11003  seq3coll  11082  s1fv  11179  ccat1st1st  11193  swrdfv  11206  pfxfv  11237  swrdswrd  11258  shftcan1  11366  shftcan2  11367  shftvalg  11368  shftval4g  11369  climshft2  11838  sumeq2  11891  summodc  11915  zsumdc  11916  fsum3  11919  isumz  11921  fisumss  11924  fsum3cvg2  11926  isumsplit  12023  prodeq2w  12088  prodeq2  12089  prodmodc  12110  zproddc  12111  fprodseq  12115  prod1dc  12118  fprodssdc  12122  nninfctlemfo  12582  odzval  12785  1arithlem2  12908  fvsetsid  13087  setsslid  13104  setsslnid  13105  prdsex  13323  prdsval  13327  prdsplusgfval  13338  prdsmulrfval  13340  imasival  13360  imasbas  13361  imasplusg  13362  imasmulr  13363  igsumvalx  13443  gsumfzval  13445  gsumpropd  13446  gsumress  13449  gsumval2  13451  grpinvval  13597  grpsubfvalg  13599  grpsubpropdg  13658  grpsubpropd2  13659  pwsinvg  13666  mulgfvalg  13679  mulgpropdg  13722  submmulg  13724  subgmulg  13746  releqgg  13778  eqgex  13779  eqgfval  13780  gsumfzmptfidmadd  13897  unitinvcl  14108  unitinvinv  14109  unitlinv  14111  unitrinv  14112  unitnegcl  14115  dvrfvald  14118  dvrvald  14119  rdivmuldivd  14129  subrgugrp  14225  lspval  14375  ixpsnbasval  14451  lidlnegcl  14470  rspcl  14476  rspssid  14477  rspssp  14479  rspsn  14519  zrhmulg  14605  znzrhval  14632  mplsubgfilemm  14683  mplsubgfilemcl  14684  mplsubgfileminv  14685  mplnegfi  14690  ntrval  14805  clsval  14806  neival  14838  cnpval  14893  txmetcnp  15213  metcnpd  15215  limccl  15354  ellimc3apf  15355  cnplimclemr  15364  limccnp2cntop  15372  dvfvalap  15376  dvfre  15405  plycoeid3  15452  plyrecj  15458  lgsval4  15720  lgsmod  15726  vtxdgfval  16074  vtxdgfifival  16077  vtxdgop  16078  vtxdeqd  16082  vtxdfifiun  16083  wksfval  16094  wlkres  16149  2omap  16472  pw1map  16474  peano4nninf  16486