Theorem fveq1d 5496

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 5493	. 2 |- ( F = G -> ( F ` A ) = ( G ` A ) )
3	1, 2	syl 14	1 |- ( ph -> ( F ` A ) = ( G ` A ) )

Syntax hints:   -> wi 4   = wceq 1348   ` cfv 5196

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 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-tru 1351  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-rex 2454  df-uni 3795  df-br 3988  df-iota 5158  df-fv 5204

This theorem is referenced by:  fveq12d  5501  funssfv  5520  csbfv2g  5531  fvco4  5566  fvmptd  5575  fvmpt2d  5580  mpteqb  5584  fvmptt  5585  fnmptfvd  5598  fmptco  5660  fvunsng  5688  fvsng  5690  fsnunfv  5695  f1ocnvfv1  5754  f1ocnvfv2  5755  fcof1  5760  fcofo  5761  ofvalg  6068  offval2  6074  ofrfval2  6075  caofinvl  6081  tfrlemi1  6309  rdg0g  6365  freceq1  6369  oav  6431  omv  6432  oeiv  6433  mapxpen  6824  xpmapenlem  6825  nninfisollemne  7105  nninfisol  7107  exmidomni  7116  cc3  7223  fseq1p1m1  10043  seqeq3  10399  seq3f1olemqsum  10449  seq3f1olemstep  10450  seq3f1olemp  10451  seq3id  10457  seq3z  10460  exp3val  10471  bcval5  10690  bcn2  10691  seq3coll  10770  shftcan1  10791  shftcan2  10792  shftvalg  10793  shftval4g  10794  climshft2  11262  sumeq2  11315  summodc  11339  zsumdc  11340  fsum3  11343  isumz  11345  fisumss  11348  fsum3cvg2  11350  isumsplit  11447  prodeq2w  11512  prodeq2  11513  prodmodc  11534  zproddc  11535  fprodseq  11539  prod1dc  11542  fprodssdc  11546  odzval  12188  1arithlem2  12309  fvsetsid  12443  setsslid  12459  setsslnid  12460  ntrval  12869  clsval  12870  neival  12902  cnpval  12957  txmetcnp  13277  metcnpd  13279  limccl  13387  ellimc3apf  13388  cnplimclemr  13397  limccnp2cntop  13405  dvfvalap  13409  dvfre  13433  lgsval4  13680  lgsmod  13686  peano4nninf  14004