Theorem fveq1d 5697

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

This proof depends on syntax axioms:   -> wi 4   = wceq 1402   ` cfv 5377

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-rex 2534  df-uni 3936  df-br 4131  df-iota 5337  df-fv 5385

This theorem is used by:  fveq12d  5702  funssfv  5721  fv2prc  5735  csbfv2g  5737  fvco4  5777  fvmptd  5786  fvmpt2d  5792  mpteqb  5796  fvmptt  5797  fnmptfvd  5813  fmptco  5874  fvunsng  5909  fvsng  5911  fsnunfv  5916  f1ocnvfv1  5983  f1ocnvfv2  5984  fcof1  5989  fcofo  5990  ofvalg  6312  offval2  6318  ofrfval2  6319  caofinvl  6328  tfrlemi1  6603  rdg0g  6659  freceq1  6663  oav  6727  omv  6728  oeiv  6729  pw2f1odclem  7134  mapxpen  7148  xpmapenlem  7149  2omap  7318  nninfisollemne  7471  nninfisol  7473  exmidomni  7482  nninfwlpoimlemginf  7516  cc3  7634  indval0  9297  fseq1p1m1  10501  seqeq3  10889  seq3f1olemqsum  10950  seq3f1olemstep  10951  seq3f1olemp  10952  seqf1oglem2  10957  seqf1og  10958  seq3id  10962  seq3z  10965  exp3val  10978  bcval5  11201  bcn2  11202  hashf1lem1  11285  seq3coll  11294  s1fv  11394  ccat1st1st  11409  ccat2s1fvwd  11415  swrdfv  11425  pfxfv  11456  swrdswrd  11477  shftcan1  11599  shftcan2  11600  shftvalg  11601  shftval4g  11602  climshft2  12072  sumeq2  12125  summodc  12150  zsumdc  12151  fsum3  12154  isumz  12156  fisumss  12159  fsum3cvg2  12161  isumsplit  12258  prodeq2w  12323  prodeq2  12324  prodmodc  12345  zproddc  12346  fprodseq  12350  prod1dc  12353  fprodssdc  12357  nninfctlemfo  12817  odzval  13020  1arithlem2  13143  ballotfileme  13236  ballotfilemi  13243  ballotfi  13282  fvsetsid  13386  setsslid  13403  setsslnid  13404  imasival  13627  imasbas  13628  imasplusg  13629  imasmulr  13630  gzsumvalx  13709  gzsumfzval  13711  gzsumress  13712  gzsumval2  13714  grpinvval  13848  grpsubfvalg  13850  grpsubpropdg  13909  grpsubpropd2  13910  mulgfvalg  13924  mulgpropdg  13967  submmulg  13969  subgmulg  13991  releqgg  14023  eqgex  14024  eqgfval  14025  gzsumshift  14149  prdsex  14172  prdsval  14173  prdsplusgfval  14184  prdsmulrfval  14186  pwsinvg  14215  unitinvcl  14430  unitinvinv  14431  unitlinv  14433  unitrinv  14434  unitnegcl  14437  dvrfvald  14440  dvrvald  14441  rdivmuldivd  14451  subrgugrp  14548  rrgsupp  14574  opprdrng  14620  lspval  14727  ixpsnbasval  14803  lidlnegcl  14822  rspcl  14828  rspssid  14829  rspssp  14831  rspsn  14871  zrhmulg  14955  znzrhval  14982  aspval  15015  mplsubgfilemm  15089  mplsubgfilemcl  15090  mplsubgfileminv  15091  mplnegfi  15096  ntrval  15211  clsval  15212  neival  15244  cnpval  15299  txmetcnp  15619  metcnpd  15621  limccl  15760  ellimc3apf  15761  cnplimclemr  15770  limccnp2cntop  15778  dvfvalap  15782  dvfre  15811  plycoeid3  15858  plyrecj  15864  lgsval4  16139  lgsmod  16145  uhgrspansubgrlem  16517  vtxdgfval  16529  vtxdgfifival  16532  vtxdgop  16533  vtxdeqd  16537  vtxdfifiun  16538  1loopgrvd0fi  16547  1hevtxdg0fi  16548  1hevtxdg1en  16549  1hegrvtxdg1fi  16550  wksfval  16563  wlkres  16620  eupth2fi  16720  pw1map  17025  peano4nninf  17049