Theorem fveq1d 5416

Description: Equality deduction for function value. (Contributed by NM, 2-Sep-2003.)

Hypothesis

Ref	Expression
fveq1d.1	|- ( ph -> F = G )

Assertion

Ref	Expression
fveq1d	|- ( ph -> ( F ` A ) = ( G ` A ) )

Proof of Theorem fveq1d

Step	Hyp	Ref	Expression
1		fveq1d.1	. 2 |- ( ph -> F = G )
2		fveq1 5413	. 2 |- ( F = G -> ( F ` A ) = ( G ` A ) )
3	1, 2	syl 14	1 |- ( ph -> ( F ` A ) = ( G ` A ) )

Syntax hints:   -> wi 4   = wceq 1331   ` cfv 5118

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 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2119

This theorem depends on definitions:  df-bi 116  df-tru 1334  df-nf 1437  df-sb 1736  df-clab 2124  df-cleq 2130  df-clel 2133  df-nfc 2268  df-rex 2420  df-uni 3732  df-br 3925  df-iota 5083  df-fv 5126

This theorem is referenced by:  fveq12d  5421  funssfv  5440  csbfv2g  5451  fvco4  5486  fvmptd  5495  fvmpt2d  5500  mpteqb  5504  fvmptt  5505  fmptco  5579  fvunsng  5607  fvsng  5609  fsnunfv  5614  f1ocnvfv1  5671  f1ocnvfv2  5672  fcof1  5677  fcofo  5678  ofvalg  5984  offval2  5990  ofrfval2  5991  caofinvl  5997  tfrlemi1  6222  rdg0g  6278  freceq1  6282  oav  6343  omv  6344  oeiv  6345  mapxpen  6735  xpmapenlem  6736  exmidomni  7007  fseq1p1m1  9867  seqeq3  10216  seq3f1olemqsum  10266  seq3f1olemstep  10267  seq3f1olemp  10268  seq3id  10274  seq3z  10277  exp3val  10288  bcval5  10502  bcn2  10503  seq3coll  10578  shftcan1  10599  shftcan2  10600  shftvalg  10601  shftval4g  10602  climshft2  11068  sumeq2  11121  summodc  11145  zsumdc  11146  fsum3  11149  isumz  11151  fisumss  11154  fsum3cvg2  11156  isumsplit  11253  prodeq2w  11318  prodeq2  11319  fvsetsid  11982  setsslid  11998  setsslnid  11999  ntrval  12268  clsval  12269  neival  12301  cnpval  12356  txmetcnp  12676  metcnpd  12678  limccl  12786  ellimc3apf  12787  cnplimclemr  12796  limccnp2cntop  12804  dvfvalap  12808  dvfre  12832  peano4nninf  13189