Theorem fveq1d 5487

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

Syntax hints:   → wi 4   = wceq 1343  ‘cfv 5187

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1435  ax-7 1436  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-8 1492  ax-10 1493  ax-11 1494  ax-i12 1495  ax-bndl 1497  ax-4 1498  ax-17 1514  ax-i9 1518  ax-ial 1522  ax-i5r 1523  ax-ext 2147

This theorem depends on definitions:  df-bi 116  df-tru 1346  df-nf 1449  df-sb 1751  df-clab 2152  df-cleq 2158  df-clel 2161  df-nfc 2296  df-rex 2449  df-uni 3789  df-br 3982  df-iota 5152  df-fv 5195

This theorem is referenced by:  fveq12d  5492  funssfv  5511  csbfv2g  5522  fvco4  5557  fvmptd  5566  fvmpt2d  5571  mpteqb  5575  fvmptt  5576  fmptco  5650  fvunsng  5678  fvsng  5680  fsnunfv  5685  f1ocnvfv1  5744  f1ocnvfv2  5745  fcof1  5750  fcofo  5751  ofvalg  6058  offval2  6064  ofrfval2  6065  caofinvl  6071  tfrlemi1  6296  rdg0g  6352  freceq1  6356  oav  6418  omv  6419  oeiv  6420  mapxpen  6810  xpmapenlem  6811  nninfisollemne  7091  nninfisol  7093  exmidomni  7102  cc3  7205  fseq1p1m1  10025  seqeq3  10381  seq3f1olemqsum  10431  seq3f1olemstep  10432  seq3f1olemp  10433  seq3id  10439  seq3z  10442  exp3val  10453  bcval5  10672  bcn2  10673  seq3coll  10751  shftcan1  10772  shftcan2  10773  shftvalg  10774  shftval4g  10775  climshft2  11243  sumeq2  11296  summodc  11320  zsumdc  11321  fsum3  11324  isumz  11326  fisumss  11329  fsum3cvg2  11331  isumsplit  11428  prodeq2w  11493  prodeq2  11494  prodmodc  11515  zproddc  11516  fprodseq  11520  prod1dc  11523  fprodssdc  11527  odzval  12169  1arithlem2  12290  fvsetsid  12424  setsslid  12440  setsslnid  12441  ntrval  12710  clsval  12711  neival  12743  cnpval  12798  txmetcnp  13118  metcnpd  13120  limccl  13228  ellimc3apf  13229  cnplimclemr  13238  limccnp2cntop  13246  dvfvalap  13250  dvfre  13274  lgsval4  13521  lgsmod  13527  peano4nninf  13846