Theorem fveq1d 5472

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

Syntax hints:   → wi 4   = wceq 1335  ‘cfv 5172

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 1427  ax-7 1428  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-8 1484  ax-10 1485  ax-11 1486  ax-i12 1487  ax-bndl 1489  ax-4 1490  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2139

This theorem depends on definitions:  df-bi 116  df-tru 1338  df-nf 1441  df-sb 1743  df-clab 2144  df-cleq 2150  df-clel 2153  df-nfc 2288  df-rex 2441  df-uni 3775  df-br 3968  df-iota 5137  df-fv 5180

This theorem is referenced by:  fveq12d  5477  funssfv  5496  csbfv2g  5507  fvco4  5542  fvmptd  5551  fvmpt2d  5556  mpteqb  5560  fvmptt  5561  fmptco  5635  fvunsng  5663  fvsng  5665  fsnunfv  5670  f1ocnvfv1  5729  f1ocnvfv2  5730  fcof1  5735  fcofo  5736  ofvalg  6043  offval2  6049  ofrfval2  6050  caofinvl  6056  tfrlemi1  6281  rdg0g  6337  freceq1  6341  oav  6403  omv  6404  oeiv  6405  mapxpen  6795  xpmapenlem  6796  nninfisollemne  7076  nninfisol  7078  exmidomni  7087  cc3  7190  fseq1p1m1  10002  seqeq3  10358  seq3f1olemqsum  10408  seq3f1olemstep  10409  seq3f1olemp  10410  seq3id  10416  seq3z  10419  exp3val  10430  bcval5  10648  bcn2  10649  seq3coll  10724  shftcan1  10745  shftcan2  10746  shftvalg  10747  shftval4g  10748  climshft2  11214  sumeq2  11267  summodc  11291  zsumdc  11292  fsum3  11295  isumz  11297  fisumss  11300  fsum3cvg2  11302  isumsplit  11399  prodeq2w  11464  prodeq2  11465  prodmodc  11486  zproddc  11487  fprodseq  11491  prod1dc  11494  fprodssdc  11498  odzval  12131  fvsetsid  12294  setsslid  12310  setsslnid  12311  ntrval  12580  clsval  12581  neival  12613  cnpval  12668  txmetcnp  12988  metcnpd  12990  limccl  13098  ellimc3apf  13099  cnplimclemr  13108  limccnp2cntop  13116  dvfvalap  13120  dvfre  13144  peano4nninf  13649