Theorem fveq1d 5431

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

Syntax hints:   → wi 4   = wceq 1332  ‘cfv 5131

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 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122

This theorem depends on definitions:  df-bi 116  df-tru 1335  df-nf 1438  df-sb 1737  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-rex 2423  df-uni 3745  df-br 3938  df-iota 5096  df-fv 5139

This theorem is referenced by:  fveq12d  5436  funssfv  5455  csbfv2g  5466  fvco4  5501  fvmptd  5510  fvmpt2d  5515  mpteqb  5519  fvmptt  5520  fmptco  5594  fvunsng  5622  fvsng  5624  fsnunfv  5629  f1ocnvfv1  5686  f1ocnvfv2  5687  fcof1  5692  fcofo  5693  ofvalg  5999  offval2  6005  ofrfval2  6006  caofinvl  6012  tfrlemi1  6237  rdg0g  6293  freceq1  6297  oav  6358  omv  6359  oeiv  6360  mapxpen  6750  xpmapenlem  6751  exmidomni  7022  cc3  7100  fseq1p1m1  9905  seqeq3  10254  seq3f1olemqsum  10304  seq3f1olemstep  10305  seq3f1olemp  10306  seq3id  10312  seq3z  10315  exp3val  10326  bcval5  10541  bcn2  10542  seq3coll  10617  shftcan1  10638  shftcan2  10639  shftvalg  10640  shftval4g  10641  climshft2  11107  sumeq2  11160  summodc  11184  zsumdc  11185  fsum3  11188  isumz  11190  fisumss  11193  fsum3cvg2  11195  isumsplit  11292  prodeq2w  11357  prodeq2  11358  prodmodc  11379  zproddc  11380  fprodseq  11384  fvsetsid  12032  setsslid  12048  setsslnid  12049  ntrval  12318  clsval  12319  neival  12351  cnpval  12406  txmetcnp  12726  metcnpd  12728  limccl  12836  ellimc3apf  12837  cnplimclemr  12846  limccnp2cntop  12854  dvfvalap  12858  dvfre  12882  peano4nninf  13375